chore: avoid superfluous use of push_neg with contrapose, by_contra o… (#37937)

…r by_cases

Found by the linter in #37907.

Author: grunweg

Archive/Imo/Imo1988Q6.lean

@@ -179,7 +179,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
     suffices hc : c ≠ mx from lt_of_le_of_ne (mod_cast c_lt) hc
     -- However, recall that B(m_x) ≠ m_x + m_y.
     -- If c = m_x, we can prove B(m_x) = m_x + m_y.
-    contrapose! hm_B₂
+    contrapose hm_B₂
     subst c
     simp [hV₁]
     -- Hence p' = (c, m_x) lies on the upper branch, and we are done.

Archive/Imo/Imo2008Q2.lean

@@ -46,9 +46,9 @@ theorem imo2008_q2a (x y z : ℝ) (h : x * y * z = 1) (hx : x ≠ 1) (hy : y ≠
     x ^ 2 / (x - 1) ^ 2 + y ^ 2 / (y - 1) ^ 2 + z ^ 2 / (z - 1) ^ 2 ≥ 1 := by
   obtain ⟨a, b, c, ha, hb, hc, rfl, rfl, rfl⟩ := subst_abc h
   obtain ⟨m, n, rfl, rfl⟩ : ∃ m n, b = c - m ∧ a = c - m - n := by use c - b, b - a; simp
-  have hm_ne_zero : m ≠ 0 := by contrapose! hy; simpa [field]
-  have hn_ne_zero : n ≠ 0 := by contrapose! hx; simpa [field]
-  have hmn_ne_zero : m + n ≠ 0 := by contrapose! hz; field_simp; linarith
+  have hm_ne_zero : m ≠ 0 := by contrapose hy; simpa [field]
+  have hn_ne_zero : n ≠ 0 := by contrapose hx; simpa [field]
+  have hmn_ne_zero : m + n ≠ 0 := by contrapose hz; field_simp; linarith
   have hc_sub_sub : c - (c - m - n) = m + n := by abel
   rw [ge_iff_le, ← sub_nonneg]
   convert sq_nonneg ((c * (m ^ 2 + n ^ 2 + m * n) - m * (m + n) ^ 2) / (m * n * (m + n)))

Archive/MiuLanguage/DecisionNec.lean

@@ -133,7 +133,7 @@ theorem goodm_of_rule2 (xs : Miustr) (_ : Derivable (M :: xs)) (h₂ : Goodm (M
   constructor
   · rfl
   · obtain ⟨mhead, mtail⟩ := h₂
-    contrapose! mtail
+    contrapose mtail
     rw [cons_append] at mtail
     exact or_self_iff.mp (mem_append.mp mtail)
 
@@ -145,7 +145,7 @@ theorem goodm_of_rule3 (as bs : Miustr) (h₁ : Derivable (as ++ [I, I, I] ++ bs
   · cases as
     · contradiction
     exact mhead
-  · contrapose! nmtail
+  · contrapose nmtail
     rcases exists_cons_of_ne_nil k with ⟨x, xs, rfl⟩
     simp_rw [cons_append] at nmtail ⊢
     simpa using nmtail
@@ -163,7 +163,7 @@ theorem goodm_of_rule4 (as bs : Miustr) (h₁ : Derivable (as ++ [U, U] ++ bs))
   · cases as
     · contradiction
     exact mhead
-  · contrapose! nmtail
+  · contrapose nmtail
     rcases exists_cons_of_ne_nil k with ⟨x, xs, rfl⟩
     simp_rw [cons_append] at nmtail ⊢
     simpa using nmtail

Archive/Sensitivity.lean

@@ -131,7 +131,7 @@ theorem adj_iff_proj_adj {p q : Q n.succ} (h₀ : p 0 = q 0) :
     rw [← Fin.pred_inj (ha := (?ha : y ≠ 0)) (hb := (?hb : i.succ ≠ 0)),
       Fin.pred_succ]
     case ha =>
-      contrapose! hy
+      contrapose hy
       rw [hy, h₀]
     case hb =>
       apply Fin.succ_ne_zero

Archive/Wiedijk100Theorems/PerfectNumbers.lean

@@ -62,7 +62,7 @@ theorem eq_two_pow_mul_odd {n : ℕ} (hpos : 0 < n) : ∃ k m : ℕ, n = 2 ^ k *
   refine ⟨hm, ?_⟩
   rw [even_iff_two_dvd]
   have hg := h.not_pow_dvd_of_multiplicity_lt (Nat.lt_succ_self _)
-  contrapose! hg
+  contrapose hg
   rcases hg with ⟨k, rfl⟩
   apply Dvd.intro k
   rw [pow_succ, mul_assoc, ← hm]
@@ -105,7 +105,7 @@ theorem eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : Even n) (p
         apply ne_of_lt _ jcon2
         rw [mersenne, ← Nat.pred_eq_sub_one, Nat.lt_pred_iff, ← pow_one (Nat.succ 1)]
         apply pow_lt_pow_right₀ (Nat.lt_succ_self 1) (Nat.succ_lt_succ k.succ_pos)
-    contrapose! hm
+    contrapose hm
     simp [hm]
 
 /-- The Euclid-Euler theorem characterizing even perfect numbers -/

Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.lean

@@ -91,7 +91,7 @@ theorem cubic_depressed_eq_zero_iff (hω : IsPrimitiveRoot ω 3) (hp_nonzero : p
   rw [h₁]
   apply Eq.congr_left
   have hs_nonzero : s ≠ 0 := by
-    contrapose! hp_nonzero with hs_nonzero
+    contrapose hp_nonzero with hs_nonzero
     linear_combination -1 * ht + t * hs_nonzero
   rw [← mul_left_inj' (pow_ne_zero 3 hs_nonzero)]
   have H := cube_root_of_unity_sum hω
@@ -172,7 +172,7 @@ theorem quartic_depressed_eq_zero_iff
   have hi2 : (2 : K) ≠ 0 := Invertible.ne_zero _
   have h4 : (4 : K) = 2 ^ 2 := by norm_num
   have hs_nonzero : s ≠ 0 := by
-    contrapose! hq_nonzero with hs0
+    contrapose hq_nonzero with hs0
     linear_combination (exp := 2) -hu + (4 * r - u ^ 2) * hs + (u ^ 2 * s - 4 * r * s) * hs0
   calc
     _ ↔ 4 * (x ^ 4 + p * x ^ 2 + q * x + r) = 0 := by simp [h4, hi2]

Mathlib/Algebra/Algebra/Spectrum/Basic.lean

@@ -440,7 +440,7 @@ lemma spectrum.units_conjugate {a : A} {u : Aˣ} :
     simp [mul_assoc]
   intro a u μ hμ
   rw [spectrum.mem_iff] at hμ ⊢
-  contrapose! hμ
+  contrapose hμ
   simpa [mul_sub, sub_mul, Algebra.right_comm] using u.isUnit.mul hμ |>.mul u⁻¹.isUnit
 
 /-- Conjugation by a unit preserves the spectrum, inverse on left. -/

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -1013,7 +1013,7 @@ noncomputable def gcdMonoidOfGCD [DecidableEq α] (gcd : α → α → α)
       · rfl
       have h := (Classical.choose_spec ((gcd_dvd_left a 0).trans (Dvd.intro 0 rfl))).symm
       have a0' : gcd a 0 ≠ 0 := by
-        contrapose! a0
+        contrapose a0
         rw [← associated_zero_iff_eq_zero, ← a0]
         exact associated_of_dvd_dvd (dvd_gcd (dvd_refl a) (dvd_zero a)) (gcd_dvd_left _ _)
       apply Or.resolve_left (mul_eq_zero.1 _) a0'
@@ -1051,7 +1051,7 @@ noncomputable def normalizedGCDMonoidOfGCD [NormalizationMonoid α] [DecidableEq
           · rw [hl, zero_mul]
         have h1 : gcd a b ≠ 0 := by
           have hab : a * b ≠ 0 := mul_ne_zero a0 hb
-          contrapose! hab
+          contrapose hab
           rw [← normalize_eq_zero, ← this, hab, zero_mul]
         have h2 : normalize (gcd a b * l) = gcd a b * l := by rw [this, normalize_idem]
         rw [← normalize_gcd] at this

Mathlib/Algebra/Group/Irreducible/Indecomposable.lean

@@ -102,7 +102,7 @@ lemma Submonoid.closure_image_isMulIndecomposable_baseOf [Finite ι]
   have ⟨(hi₀ : 1 < f (v i)), (hi₁ : v i ∉ _)⟩ : i ∈ s := hi.prop
   have hi₂ (k : ι) (hk₀ : 1 < f (v k)) (hk₁ : f (v k) < f (v i)) : v k ∈ closure (v '' t) := by
     by_contra hk₂; exact not_le.mpr hk₁ <| hi.le_of_le ⟨hk₀, hk₂⟩ hk₁.le
-  have hi₃ : i ∉ t := by contrapose! hi₁; exact subset_closure <| mem_image_of_mem v hi₁
+  have hi₃ : i ∉ t := by contrapose hi₁; exact subset_closure <| mem_image_of_mem v hi₁
   obtain ⟨j, k, hj, hk, hjk⟩ : ∃ (j k : ι) (hj : 1 < f (v j)) (hk : 1 < f (v k)),
       v i = v j * v k := by
     grind [IsMulIndecomposable]

Mathlib/Algebra/Group/UniqueProds/Basic.lean

@@ -560,7 +560,7 @@ theorem of_mulOpposite (h : TwoUniqueProds Gᵐᵒᵖ) : TwoUniqueProds G where
     simp_rw [mem_product] at h1 h2 ⊢
     refine ⟨(_, _), ⟨?_, ?_⟩, (_, _), ⟨?_, ?_⟩, ?_, hu1.of_mulOpposite, hu2.of_mulOpposite⟩
     pick_goal 5
-    · contrapose! hne; rw [Prod.ext_iff] at hne ⊢
+    · contrapose hne; rw [Prod.ext_iff] at hne ⊢
       exact ⟨unop_injective hne.2, unop_injective hne.1⟩
     all_goals apply (mem_map' f).mp
     exacts [h1.2, h1.1, h2.2, h2.1]