chore: avoid superfluous use of push_neg with contrapose or by_contra

Found by #37907.

Author: grunweg

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]

Mathlib/Algebra/GroupWithZero/Associated.lean

@@ -338,7 +338,7 @@ theorem Associated.of_pow_associated_of_prime' [CommMonoidWithZero M] [IsCancelM
 lemma Irreducible.isRelPrime_iff_not_dvd [Monoid M] {p n : M} (hp : Irreducible p) :
     IsRelPrime p n ↔ ¬ p ∣ n := by
   refine ⟨fun h contra ↦ hp.not_isUnit (h dvd_rfl contra), fun hpn d hdp hdn ↦ ?_⟩
-  contrapose! hpn
+  contrapose hpn
   suffices Associated p d from this.dvd.trans hdn
   exact (hp.dvd_iff.mp hdp).resolve_left hpn
 
@@ -669,7 +669,7 @@ theorem dvdNotUnit_of_lt {a b : Associates M} (hlt : a < b) : DvdNotUnit a b :=
     apply dvd_zero
   rcases hlt with ⟨⟨x, rfl⟩, ndvd⟩
   refine ⟨x, ?_, rfl⟩
-  contrapose! ndvd
+  contrapose ndvd
   rcases ndvd with ⟨u, rfl⟩
   simp
 

Mathlib/Algebra/Lie/Semisimple/Basic.lean

@@ -86,7 +86,7 @@ instance : LieModule.IsIrreducible R L L := by
   suffices Nontrivial (LieIdeal R L) from ⟨IsSimple.eq_bot_or_eq_top⟩
   rw [LieSubmodule.nontrivial_iff, ← not_subsingleton_iff_nontrivial]
   have _i : ¬ IsLieAbelian L := IsSimple.non_abelian R
-  contrapose! _i
+  contrapose _i
   infer_instance
 
 protected lemma isAtom_top : IsAtom (⊤ : LieIdeal R L) := isAtom_top
@@ -185,7 +185,7 @@ lemma isSimple_of_isAtom (I : LieIdeal R L) (hI : IsAtom I) : IsSimple R I where
       exact x.2
     -- So we need to show `J ≠ I` as ideals of `L`.
     -- This follows from our assumption that `J ≠ ⊤` as ideals of `I`.
-    contrapose! hJ
+    contrapose hJ
     rw [eq_top_iff]
     rintro ⟨x, hx⟩ -
     rw [← hJ] at hx
@@ -260,7 +260,7 @@ lemma finitelyAtomistic : ∀ s : Finset (LieIdeal R L), ↑s ⊆ {I : LieIdeal
     exact LieSubmodule.lie_mem_lie j.2 hx
   -- Indeed `J ⊓ I = ⊥`, since `J` is an atom that is not contained in `I`.
   apply ((hs hJs).le_iff.mp _).resolve_right
-  · contrapose! hJI
+  · contrapose hJI
     rw [← hJI]
     exact inf_le_right
   exact inf_le_left

Mathlib/Algebra/Lie/Sl2.lean

@@ -65,12 +65,12 @@ lemma lie_lie_smul_f (t : IsSl2Triple h e f) : ⁅h, f⁆ = -((2 : R) • f) :=
 
 lemma e_ne_zero (t : IsSl2Triple h e f) : e ≠ 0 := by
   have := t.h_ne_zero
-  contrapose! this
+  contrapose this
   simpa [this] using t.lie_e_f.symm
 
 lemma f_ne_zero (t : IsSl2Triple h e f) : f ≠ 0 := by
   have := t.h_ne_zero
-  contrapose! this
+  contrapose this
   simpa [this] using t.lie_e_f.symm
 
 variable {R}

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -278,7 +278,7 @@ def equivSetOf : Weight R L M ≃ {χ : L → R | genWeightSpace M χ ≠ ⊥} w
 lemma genWeightSpaceOf_ne_bot (χ : Weight R L M) (x : L) :
     genWeightSpaceOf M (χ x) x ≠ ⊥ := by
   have : ⨅ x, genWeightSpaceOf M (χ x) x ≠ ⊥ := χ.genWeightSpace_ne_bot
-  contrapose! this
+  contrapose this
   rw [eq_bot_iff]
   exact le_of_le_of_eq (iInf_le _ _) this
 

Mathlib/Algebra/Lie/Weights/Killing.lean

@@ -440,7 +440,7 @@ lemma disjoint_ker_weight_corootSpace (α : Weight K H L) :
 
 lemma root_apply_cartanEquivDual_symm_ne_zero {α : Weight K H L} (hα : α.IsNonZero) :
     α ((cartanEquivDual H).symm α) ≠ 0 := by
-  contrapose! hα
+  contrapose hα
   suffices (cartanEquivDual H).symm α ∈ α.ker ⊓ corootSpace α by
     rw [(disjoint_ker_weight_corootSpace α).eq_bot] at this
     simpa using this
@@ -540,7 +540,7 @@ lemma traceForm_eq_zero_of_mem_ker_of_mem_span_coroot {α : Weight K H L} {x y :
     simp [hα.eq, hβ.eq]
   else
     have hβ : β.IsNonZero := by
-      contrapose! hα
+      contrapose hα
       simp only [← coroot_eq_zero_iff] at hα ⊢
       rwa [hyp]
     have : α.ker = β.ker := by
@@ -600,7 +600,7 @@ lemma _root_.IsSl2Triple.h_eq_coroot {α : Weight K H L} (hα : α.IsNonZero)
   use (2 • (α α')⁻¹) * (killingForm K L e f)⁻¹
   have hef₀ : killingForm K L e f ≠ 0 := by
     have := ht.h_ne_zero
-    contrapose! this
+    contrapose this
     simpa [this] using h_eq
   rw [h_eq, smul_smul, mul_assoc, inv_mul_cancel₀ hef₀, mul_one, smul_assoc, coroot]
 

Mathlib/Algebra/Module/Submodule/Union.lean

@@ -43,7 +43,7 @@ lemma Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt (s : Finset ι) (p :
     · simpa using h₁ j
     replace h₂ : s.card + 1 < ENat.card K := by simpa [Finset.card_insert_of_notMem hj] using h₂
     specialize hj' (lt_trans ENat.natCast_lt_succ h₂)
-    contrapose! hj'
+    contrapose hj'
     replace hj' : (p j : Set M) ∪ (⋃ i ∈ s, p i) = univ := by
       simpa only [Finset.mem_insert, iUnion_iUnion_eq_or_left] using hj'
     suffices (p j : Set M) ⊆ ⋃ i ∈ s, p i by rwa [union_eq_right.mpr this] at hj'