chore: avoid superfluous use of push_neg

grunweg · grunweg · commit bbd7d9be8d4b · 2026-04-10T23:50:28.000+02:00
Not exhaustive yet; found by leanprover-community#37907.
diff --git a/Mathlib/Algebra/GCDMonoid/Basic.lean b/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
diff --git a/Mathlib/Algebra/GroupWithZero/Associated.lean b/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
 
diff --git a/Mathlib/Algebra/Tropical/Lattice.lean b/Mathlib/Algebra/Tropical/Lattice.lean
@@ -68,14 +68,14 @@ instance [ConditionallyCompleteLinearOrder R] : ConditionallyCompleteLinearOrder
       have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm
       simp only [sSup, Set.image_empty, trop_inj_iff]
       apply csSup_of_not_bddAbove
-      contrapose! hs
+      contrapose hs
       change BddAbove (tropOrderIso.symm '' s) at hs
       exact tropOrderIso.symm.bddAbove_image.1 hs
     csInf_of_not_bddBelow := by
       intro s hs
       have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm
       simp only [sInf, Set.image_empty, trop_inj_iff]
       apply csInf_of_not_bddBelow
-      contrapose! hs
+      contrapose hs
       change BddBelow (tropOrderIso.symm '' s) at hs
       exact tropOrderIso.symm.bddBelow_image.1 hs }
diff --git a/Mathlib/Data/Finset/Insert.lean b/Mathlib/Data/Finset/Insert.lean
@@ -433,7 +433,7 @@ instance (i : α) (s : Finset α) : Nonempty ((insert i s : Finset α) : Set α)
   (Finset.coe_nonempty.mpr (s.insert_nonempty i)).to_subtype
 
 theorem ne_insert_of_notMem (s t : Finset α) {a : α} (h : a ∉ s) : s ≠ insert a t := by
-  contrapose! h
+  contrapose h
   simp [h]
 
 theorem insert_subset_iff : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t := by grind
diff --git a/Mathlib/Data/Finsupp/Fin.lean b/Mathlib/Data/Finsupp/Fin.lean
@@ -79,11 +79,11 @@ theorem cons_zero_zero : cons 0 (0 : Fin n →₀ M) = 0 := by simp [cons_zero_e
 variable {s} {y}
 
 theorem cons_ne_zero_of_left (h : y ≠ 0) : cons y s ≠ 0 := by
-  contrapose! h with c
+  contrapose h with c
   rw [← cons_zero y s, c, Finsupp.coe_zero, Pi.zero_apply]
 
 theorem cons_ne_zero_of_right (h : s ≠ 0) : cons y s ≠ 0 := by
-  contrapose! h with c
+  contrapose h with c
   ext a
   simp [← cons_succ a y s, c]
 
diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
@@ -591,7 +591,7 @@ theorem succ_idxOf_lt_length_of_mem_dropLast {l : List α} {a : α} (ha : a ∈
 theorem idxOf_getLast {l : List α} (hl : l ≠ []) (hl' : l.getLast hl ∉ l.dropLast) :
     l.idxOf (l.getLast hl) = l.length - 1 :=
   Nat.le_antisymm (Nat.le_pred_of_lt <| l.idxOf_lt_length_of_mem <| getLast_mem hl) <| by
-    contrapose! hl'
+    contrapose hl'
     rwa [mem_dropLast_iff_idxOf_lt <| getLast_mem hl, ← Nat.not_le]
 
 end IndexOf
diff --git a/Mathlib/Data/Nat/Count.lean b/Mathlib/Data/Nat/Count.lean
@@ -107,7 +107,7 @@ theorem count_strict_mono {m n : ℕ} (hm : p m) (hmn : m < n) : count p m < cou
   (count_lt_count_succ_iff.2 hm).trans_le <| count_monotone _ (Nat.succ_le_iff.2 hmn)
 
 theorem count_injective {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n) : m = n := by
-  by_contra! h : m ≠ n
+  by_contra h : m ≠ n
   wlog hmn : m < n
   · exact this hn hm heq.symm h.symm (by grind)
   · simpa [heq] using count_strict_mono hm hmn
diff --git a/Mathlib/Data/Set/Finite/Basic.lean b/Mathlib/Data/Set/Finite/Basic.lean
@@ -897,7 +897,7 @@ theorem not_injOn_infinite_finite_image {f : α → β} {s : Set α} (h_inf : s.
   have : Infinite s := infinite_coe_iff.mpr h_inf
   have h := not_injective_infinite_finite
             ((f '' s).codRestrict (s.restrict f) fun x => ⟨x, x.property, rfl⟩)
-  contrapose! h
+  contrapose h
   rwa [injective_codRestrict, ← injOn_iff_injective]
 
 theorem finite_range_findGreatest {P : α → ℕ → Prop} [∀ x, DecidablePred (P x)] {b : ℕ} :
diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
@@ -561,7 +561,7 @@ instance decidablePred_mem_diagSet (α : Type u) [DecidableEq α] : DecidablePre
   IsDiag.decidablePred _
 
 theorem other_ne {a : α} {z : Sym2 α} (hd : ¬IsDiag z) (h : a ∈ z) : Mem.other h ≠ a := by
-  contrapose! hd
+  contrapose hd
   have h' := Sym2.other_spec h
   rw [hd] at h'
   rw [← h']
diff --git a/Mathlib/GroupTheory/GroupAction/FixedPoints.lean b/Mathlib/GroupTheory/GroupAction/FixedPoints.lean
@@ -262,7 +262,7 @@ is disjoint from `(fixedBy α g)ᶜ`, then `g` and `h` cannot commute.
 is disjoint from `(fixedBy α g)ᶜ`, then `g` and `h` cannot commute. -/]
 theorem not_commute_of_disjoint_movedBy_preimage {g h : G} (ne_one : g ≠ 1)
     (disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)) : ¬Commute g h := by
-  contrapose! ne_one with comm
+  contrapose ne_one with comm
   rwa [movedBy_mem_fixedBy_of_commute comm, disjoint_self, Set.bot_eq_empty, ← Set.compl_univ,
     compl_inj_iff, fixedBy_eq_univ_iff_eq_one] at disjoint
 
diff --git a/Mathlib/GroupTheory/Perm/ClosureSwap.lean b/Mathlib/GroupTheory/Perm/ClosureSwap.lean
@@ -49,7 +49,7 @@ theorem exists_smul_notMem_of_subset_orbit_closure (S : Set G) (T : Set α) {a :
   have key0 : ¬ closure S ≤ stabilizer G T := by
     have ⟨b, hb⟩ := nonempty
     obtain ⟨σ, rfl⟩ := subset hb
-    contrapose! notMem with h
+    contrapose notMem with h
     exact smul_mem_smul_set_iff.mp ((h σ.2).symm ▸ hb)
   contrapose! key0
   refine (closure_le _).mpr fun σ hσ ↦ ?_
diff --git a/Mathlib/Order/Cofinal.lean b/Mathlib/Order/Cofinal.lean
@@ -145,7 +145,7 @@ theorem BddAbove.of_not_isCofinal {s : Set α} (h : ¬ IsCofinal s) : BddAbove s
   exact ⟨x, fun y hy ↦ (h y hy).le⟩
 
 theorem IsCofinal.of_not_bddAbove {s : Set α} (h : ¬ BddAbove s) : IsCofinal s := by
-  contrapose! h
+  contrapose h
   exact .of_not_isCofinal h
 
 /-- In a linear order with no maximum, cofinal sets are the same as unbounded sets. -/
diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
@@ -419,7 +419,7 @@ theorem csInf_lt_iff (hb : BddBelow s) (hs : s.Nonempty) : sInf s < a ↔ ∃ b
 
 lemma csSup_eq_univ_of_not_bddAbove (hs : ¬BddAbove s) : sSup s = sSup univ := by
   rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := univ)]
-  contrapose! hs
+  contrapose hs
   exact hs.mono (subset_univ _)
 
 lemma ciSup_eq_univ_of_not_bddAbove (hf : ¬BddAbove (range f)) : ⨆ i, f i = sSup univ :=
diff --git a/Mathlib/Order/Filter/Map.lean b/Mathlib/Order/Filter/Map.lean
@@ -442,7 +442,7 @@ theorem comap_bot : comap m ⊥ = ⊥ :=
 
 theorem neBot_of_comap (h : (comap m g).NeBot) : g.NeBot := by
   rw [neBot_iff] at *
-  contrapose! h
+  contrapose h
   rw [h]
   exact comap_bot
 
diff --git a/Mathlib/Order/Partition/Basic.lean b/Mathlib/Order/Partition/Basic.lean
@@ -194,7 +194,7 @@ lemma existsUnique_of_mem_le (h : P ≤ Q) (hx : x ∈ P) :
   obtain ⟨y, hy, hxy⟩ := h hx
   refine ⟨y, ⟨hy, hxy⟩, fun z ⟨hz, hxz⟩ => Q.eq_of_not_disjoint hz hy ?_⟩
   have := P.ne_bot_of_mem hx
-  contrapose! this
+  contrapose this
   exact le_bot_iff.mp (this hxz hxy)
 
 /-- The top partition of `s` is the partition with the single part `s`. -/
diff --git a/Mathlib/Order/PrimeSeparator.lean b/Mathlib/Order/PrimeSeparator.lean
@@ -120,7 +120,7 @@ theorem prime_ideal_of_disjoint_filter_ideal (hFI : Disjoint (F : Set α) (I : S
   have ba₁a₂F : b ⊔ (a₁ ⊓ a₂) ∈ F := PFilter.mem_of_le ineq (PFilter.inf_mem c₁F c₂F)
   -- Now, if we would have a₁ ⊓ a₂ ∈ J, then, since J is an ideal and b ∈ J, we would also get
   -- b ⊔ (a₁ ⊓ a₂) ∈ J. But this contradicts that J is disjoint from F.
-  contrapose! JF with ha₁a₂
+  contrapose JF with ha₁a₂
   rw [Set.not_disjoint_iff]
   use b ⊔ (a₁ ⊓ a₂)
   exact ⟨ba₁a₂F, sup_mem bJ ha₁a₂⟩
diff --git a/Mathlib/Order/SuccPred/Archimedean.lean b/Mathlib/Order/SuccPred/Archimedean.lean
@@ -247,7 +247,7 @@ lemma SuccOrder.forall_ne_bot_iff
     (∀ i, i ≠ ⊥ → P i) ↔ (∀ i, P (SuccOrder.succ i)) := by
   refine ⟨fun h i ↦ h _ (Order.succ_ne_bot i), fun h i hi ↦ ?_⟩
   obtain ⟨j, rfl⟩ := exists_succ_iterate_of_le (bot_le : ⊥ ≤ i)
-  have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose! hi; simp [hi]
+  have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose hi; simp [hi]
   rw [← Nat.succ_pred_eq_of_pos hj]
   simp only [Function.iterate_succ', Function.comp_apply]
   apply h
diff --git a/Mathlib/Order/SuccPred/IntervalSucc.lean b/Mathlib/Order/SuccPred/IntervalSucc.lean
@@ -40,7 +40,7 @@ theorem biUnion_Ici_Ico_map_succ [SuccOrder α] [IsSuccArchimedean α] [LinearOr
   apply subset_antisymm <|
     iUnion₂_subset fun i hi ↦ Ico_subset_Ico_left (hf i hi) |>.trans Ico_subset_Ici_self
   intro b hb
-  contrapose! h2f
+  contrapose h2f
   use b
   simp only [upperBounds, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
   exact Succ.rec (P := fun i _ ↦ f i ≤ b) hb (by simp_all)
@@ -53,7 +53,7 @@ theorem biUnion_Ici_Ioc_map_succ [SuccOrder α] [IsSuccArchimedean α] [LinearOr
   apply subset_antisymm <|
     iUnion₂_subset fun i hi ↦ Ioc_subset_Ioc_left (hf i hi) |>.trans Ioc_subset_Ioi_self
   intro b hb
-  contrapose! h2f
+  contrapose h2f
   suffices ∀ i, a ≤ i → f i < b from ⟨b, by aesop (add simp [upperBounds, le_of_lt])⟩
   exact Succ.rec (P := fun i _ ↦ f i < b) hb (by simp_all)
 
diff --git a/Mathlib/Order/SuccPred/Tree.lean b/Mathlib/Order/SuccPred/Tree.lean
@@ -196,7 +196,7 @@ lemma RootedTree.mem_subtrees_disjoint_iff {t₁ t₂ : SubRootedTree t}
     exact t₁.root_ne_bot_of_mem_subtrees ht₁ this
   mpr h := by
     rw [SubRootedTree.mem_iff] at h₁ h₂
-    contrapose! h
+    contrapose h
     rw [disjoint_iff, ← ne_eq, ← bot_lt_iff_ne_bot] at h
     rcases lt_or_le_of_directed (by simp : v₁ ⊓ v₂ ≤ v₁) h₁ with oh | oh
     · simp_all [RootedTree.subtrees, IsAtom.lt_iff]
diff --git a/Mathlib/SetTheory/Cardinal/Order.lean b/Mathlib/SetTheory/Cardinal/Order.lean
@@ -540,7 +540,7 @@ lemma exists_eq_of_iSup_eq_of_not_isSuccPrelimit
     (h : ⨆ i : ι, f i = ω) : ∃ i, f i = ω := by
   subst h
   suffices BddAbove (range f) from (isLUB_csSup' this).mem_of_not_isSuccPrelimit hω
-  contrapose! hω with hf
+  contrapose hω with hf
   rw [iSup, csSup_of_not_bddAbove hf, csSup_empty]
   exact isSuccPrelimit_bot
 
diff --git a/Mathlib/Tactic/Order/ToInt.lean b/Mathlib/Tactic/Order/ToInt.lean
@@ -60,7 +60,7 @@ theorem exists_translation : ∃ tr : Fin n → ℤ, ∀ i j, val i ≤ val j 
   · contrapose! h
     exact lt_of_le_of_ne (by simpa using (this hj.choose hi.choose (by simpa)))
       (fun h ↦ h_eq (h.symm))
-  · simpa using this hi.choose hj.choose (by apply lt_of_le_of_ne h; contrapose! h_eq; simp [h_eq])
+  · simpa using this hi.choose hj.choose (by apply lt_of_le_of_ne h; contrapose h_eq; simp [h_eq])
 
 /-- Auxiliary definition used by the `order` tactic to transfer facts in a linear order to `ℤ`. -/
 noncomputable def toInt (k : Fin n) : ℤ :=
