feat: extensible push_neg tactic

Archive/Imo/Imo1988Q6.lean

@@ -216,7 +216,7 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
   · -- Show that the claim is true if a = b.
     intro x hx
     suffices k ≤ 1 by
-      rw [Nat.le_add_one_iff, Nat.le_zero] at this
+      rw [Nat.le_one_iff_eq_zero_or_eq_one] at this
       rcases this with (rfl | rfl)
       · use 0; simp
       · use 1; simp
@@ -292,7 +292,7 @@ example {a b : ℕ} (h : a * b ∣ a ^ 2 + b ^ 2 + 1) : 3 * a * b = a ^ 2 + b ^
           omega
   · -- Show the base case.
     intro x y h h_base
-    obtain rfl | rfl : x = 0 ∨ x = 1 := by rwa [Nat.le_add_one_iff, Nat.le_zero] at h_base
+    obtain rfl | rfl : x = 0 ∨ x = 1 := Nat.le_one_iff_eq_zero_or_eq_one.mp h_base
     · simp at h
     · rw [mul_one, one_mul, add_right_comm] at h
       have y_dvd : y ∣ y * k := dvd_mul_right y k

Archive/Imo/Imo2013Q5.lean

@@ -147,7 +147,7 @@ theorem fixed_point_of_gt_1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 < x)
       (x : ℝ) + (a ^ N - x : ℚ) ≤ f x + (a ^ N - x : ℚ) := by gcongr; exact H5 x hx
       _ ≤ f x + f (a ^ N - x) := by gcongr; exact H5 _ h_big_enough
   have hxp : 0 < x := by positivity
-  have hNp : 0 < N := by by_contra! H; rw [Nat.le_zero.mp H] at hN; linarith
+  have hNp : 0 < N := by by_contra! H; rw [H] at hN; linarith
   have h2 :=
     calc
       f x + f (a ^ N - x) ≤ f (x + (a ^ N - x)) := H2 x (a ^ N - x) hxp (by positivity)

Archive/Imo/Imo2024Q3.lean

@@ -158,15 +158,14 @@ lemma apply_add_one_ne_of_apply_eq {i j : ℕ} (hi : N ≤ i) (hj : N ≤ j) (hi
     (hc.apply_add_one_lt_of_apply_eq hj h ha.symm).ne'
 
 lemma exists_infinite_setOf_apply_eq : ∃ m, {i | a i = m}.Infinite := by
-  by_contra hi
+  by_contra! hi
   have hr : (Set.range a).Infinite := by
     contrapose! hi with hr
-    rw [Set.not_infinite, ← Set.finite_coe_iff] at hr
+    rw [← Set.finite_coe_iff] at hr
     obtain ⟨n, hn⟩ := Finite.exists_infinite_fiber (Set.rangeFactorization a)
     rw [Set.infinite_coe_iff, Set.preimage] at hn
     simp only [Set.mem_singleton_iff, Set.rangeFactorization, Subtype.ext_iff] at hn
     exact ⟨↑n, hn⟩
-  simp only [not_exists, Set.not_infinite] at hi
   have hinj : Set.InjOn (fun i ↦ Nat.nth (a · = i) 0 + 1) (Set.range a \ Set.Ico 0 (M a N)) := by
     rintro _ ⟨⟨_, rfl⟩, hi⟩ _ ⟨⟨_, rfl⟩, hj⟩ h
     simp only [Set.mem_diff, Set.mem_range, Set.mem_Ico, zero_le, true_and, not_lt] at hi hj
@@ -336,7 +335,7 @@ lemma bddAbove_setOf_k_lt_card : BddAbove {m | ∀ hf : {i | a i = m}.Finite, k
 
 lemma k_pos : 0 < k a := by
   by_contra! hn
-  apply nonpos_iff_eq_zero.mp hn ▸ hc.infinite_setOf_apply_eq_k
+  apply hn ▸ hc.infinite_setOf_apply_eq_k
   convert Set.finite_empty
   ext i
   simp [(hc.pos i).ne']
@@ -627,7 +626,7 @@ lemma apply_add_one_eq_card_small_le_card_eq {i : ℕ} (hi : N' a N < i) (hib :
       rw [Nat.lt_add_one_iff, ← Small] at hts
       have ht0 : 0 < t := by
         by_contra! h0
-        simp [nonpos_iff_eq_zero.mp h0, hc.apply_ne_zero] at htr
+        simp [h0, hc.apply_ne_zero] at htr
       rw [← hc.infinite_setOf_apply_eq_iff_small ht0] at hts
       rw [← Nat.count_eq_card_filter_range] at htr
       constructor
@@ -643,11 +642,9 @@ lemma apply_add_one_eq_card_small_le_card_eq {i : ℕ} (hi : N' a N < i) (hib :
     rw [← Small] at ht hu
     have ht0 : 0 < t := by
       by_contra! h0
-      simp only [nonpos_iff_eq_zero] at h0
       simp [h0, hc.apply_ne_zero] at ht
     have hu0 : 0 < u := by
       by_contra! h0
-      simp only [nonpos_iff_eq_zero] at h0
       simp [h0, hc.apply_ne_zero] at hu
     rw [← hc.infinite_setOf_apply_eq_iff_small ht0] at ht
     rw [← hc.infinite_setOf_apply_eq_iff_small hu0] at hu

Archive/ZagierTwoSquares.lean

@@ -41,8 +41,7 @@ lemma zagierSet_lower_bound {x y z : ℕ} (h : (x, y, z) ∈ zagierSet k) : 0 <
   rw [zagierSet, mem_setOf_eq] at h
   refine ⟨?_, ?_, ?_⟩
   all_goals
-    by_contra q
-    rw [not_lt, nonpos_iff_eq_zero] at q
+    by_contra! q
     simp only [q, mul_zero, zero_mul, zero_add, add_zero] at h
   · apply_fun (· % 4) at h
     simp [mul_assoc, Nat.add_mod] at h
@@ -196,7 +195,6 @@ theorem Nat.Prime.sq_add_sq' {p : ℕ} [h : Fact p.Prime] (hp : p % 4 = 1) :
   apply sq_add_sq_of_nonempty_fixedPoints
   have key := (Equiv.Perm.card_fixedPoints_modEq (p := 2) (n := 1) (obvInvo_sq k)).symm.trans
     (Equiv.Perm.card_fixedPoints_modEq (p := 2) (n := 1) (complexInvo_sq k))
-  contrapose key
-  rw [Set.not_nonempty_iff_eq_empty] at key
+  contrapose! key
   simp_rw [k, key, Fintype.card_eq_zero, card_fixedPoints_eq_one]
   decide

Counterexamples/Phillips.lean

@@ -533,7 +533,7 @@ theorem countable_ne (Hcont : #ℝ = ℵ₁) (φ : (DiscreteCopy ℝ →ᵇ ℝ)
       ⋃ y ∈ φ.toBoundedAdditiveMeasure.discreteSupport, {x | y ∈ spf Hcont x} := by
     intro x hx
     dsimp at hx
-    rw [← Ne, ← nonempty_iff_ne_empty] at hx
+    push_neg at hx
     simp only [exists_prop, mem_iUnion, mem_setOf_eq]
     exact hx
   apply Countable.mono (Subset.trans A B)

Mathlib.lean

@@ -5249,7 +5249,8 @@ import Mathlib.Tactic.ProdAssoc
 import Mathlib.Tactic.ProjectionNotation
 import Mathlib.Tactic.Propose
 import Mathlib.Tactic.ProxyType
-import Mathlib.Tactic.PushNeg
+import Mathlib.Tactic.Push
+import Mathlib.Tactic.Push.Attr
 import Mathlib.Tactic.Qify
 import Mathlib.Tactic.RSuffices
 import Mathlib.Tactic.Recall

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -580,7 +580,7 @@ theorem MonoidHom.map_finprod {f : α → M} (g : M →* N) (hf : (mulSupport f)
     g (∏ᶠ i, f i) = ∏ᶠ i, g (f i) :=
   g.map_finprod_plift f <| hf.preimage Equiv.plift.injective.injOn
 
-@[to_additive]
+@[to_additive (attr := push)]
 theorem finprod_pow (hf : (mulSupport f).Finite) (n : ℕ) : (∏ᶠ i, f i) ^ n = ∏ᶠ i, f i ^ n :=
   (powMonoidHom n).map_finprod hf
 

Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean

@@ -545,7 +545,7 @@ theorem prod_induction_nonempty {M : Type*} [CommMonoid M] (f : α → M) (p : M
   Multiset.prod_induction_nonempty p hom (by simp [nonempty_iff_ne_empty.mp nonempty])
     (Multiset.forall_mem_map_iff.mpr base)
 
-@[to_additive]
+@[to_additive (attr := push ←)]
 theorem prod_pow (s : Finset α) (n : ℕ) (f : α → β) : ∏ x ∈ s, f x ^ n = (∏ x ∈ s, f x) ^ n :=
   Multiset.prod_map_pow
 

Mathlib/Algebra/CharP/MixedCharZero.lean

@@ -280,7 +280,7 @@ theorem isEmpty_algebraRat_iff_mixedCharZero [CharZero R] :
     IsEmpty (Algebra ℚ R) ↔ ∃ p > 0, MixedCharZero R p := by
   rw [← not_iff_not]
   push_neg
-  rw [not_isEmpty_iff, ← EqualCharZero.iff_not_mixedCharZero]
+  rw [← EqualCharZero.iff_not_mixedCharZero]
   apply EqualCharZero.nonempty_algebraRat_iff
 
 /-!

Mathlib/Algebra/Group/Action/Defs.lean

@@ -393,6 +393,7 @@ variable {M}
 section Monoid
 variable [Monoid N] [MulAction M N] [IsScalarTower M N N] [SMulCommClass M N N]
 
+@[push]
 lemma smul_pow (r : M) (x : N) : ∀ n, (r • x) ^ n = r ^ n • x ^ n
   | 0 => by simp
   | n + 1 => by rw [pow_succ', smul_pow _ _ n, smul_mul_smul_comm, ← pow_succ', ← pow_succ']

Mathlib/Algebra/Group/Basic.lean

@@ -215,7 +215,7 @@ variable [CommMonoid M] {x y z : M}
 theorem inv_unique (hy : x * y = 1) (hz : x * z = 1) : y = z :=
   left_inv_eq_right_inv (Trans.trans (mul_comm _ _) hy) hz
 
-@[to_additive nsmul_add] lemma mul_pow (a b : M) : ∀ n, (a * b) ^ n = a ^ n * b ^ n
+@[to_additive (attr := push) nsmul_add] lemma mul_pow (a b : M) : ∀ n, (a * b) ^ n = a ^ n * b ^ n
   | 0 => by rw [pow_zero, pow_zero, pow_zero, one_mul]
   | n + 1 => by rw [pow_succ', pow_succ', pow_succ', mul_pow, mul_mul_mul_comm]
 
@@ -395,7 +395,7 @@ theorem one_div_mul_one_div_rev : 1 / a * (1 / b) = 1 / (b * a) := by simp
 @[to_additive]
 theorem inv_div_left : a⁻¹ / b = (b * a)⁻¹ := by simp
 
-@[to_additive (attr := simp)]
+@[to_additive (attr := simp, push)]
 theorem inv_div : (a / b)⁻¹ = b / a := by simp
 
 @[to_additive]
@@ -413,7 +413,7 @@ instance (priority := 100) DivisionMonoid.toDivInvOneMonoid : DivInvOneMonoid α
   { DivisionMonoid.toDivInvMonoid with
     inv_one := by simpa only [one_div, inv_inv] using (inv_div (1 : α) 1).symm }
 
-@[to_additive (attr := simp)]
+@[to_additive (attr := simp, push, push ←)]
 lemma inv_pow (a : α) : ∀ n : ℕ, a⁻¹ ^ n = (a ^ n)⁻¹
   | 0 => by rw [pow_zero, pow_zero, inv_one]
   | n + 1 => by rw [pow_succ', pow_succ, inv_pow _ n, mul_inv_rev]
@@ -438,12 +438,12 @@ lemma zpow_neg (a : α) : ∀ n : ℤ, a ^ (-n) = (a ^ n)⁻¹
 lemma mul_zpow_neg_one (a b : α) : (a * b) ^ (-1 : ℤ) = b ^ (-1 : ℤ) * a ^ (-1 : ℤ) := by
   simp only [zpow_neg, zpow_one, mul_inv_rev]
 
-@[to_additive zsmul_neg]
+@[to_additive (attr := push ←) zsmul_neg]
 lemma inv_zpow (a : α) : ∀ n : ℤ, a⁻¹ ^ n = (a ^ n)⁻¹
   | (n : ℕ)    => by rw [zpow_natCast, zpow_natCast, inv_pow]
   | .negSucc n => by rw [zpow_negSucc, zpow_negSucc, inv_pow]
 
-@[to_additive (attr := simp) zsmul_neg']
+@[to_additive (attr := simp, push) zsmul_neg']
 lemma inv_zpow' (a : α) (n : ℤ) : a⁻¹ ^ n = a ^ (-n) := by rw [inv_zpow, zpow_neg]
 
 @[to_additive nsmul_zero_sub]
@@ -514,7 +514,7 @@ variable [DivisionCommMonoid α] (a b c d : α)
 
 attribute [local simp] mul_assoc mul_comm mul_left_comm div_eq_mul_inv
 
-@[to_additive neg_add]
+@[to_additive (attr := push high) neg_add]
 theorem mul_inv : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by simp
 
 @[to_additive]
@@ -589,11 +589,11 @@ theorem mul_div_mul_comm : a * b / (c * d) = a / c * (b / d) := by simp
   | (n : ℕ) => by simp_rw [zpow_natCast, mul_pow]
   | .negSucc n => by simp_rw [zpow_negSucc, ← inv_pow, mul_inv, mul_pow]
 
-@[to_additive nsmul_sub]
+@[to_additive (attr := push) nsmul_sub]
 lemma div_pow (a b : α) (n : ℕ) : (a / b) ^ n = a ^ n / b ^ n := by
   simp only [div_eq_mul_inv, mul_pow, inv_pow]
 
-@[to_additive zsmul_sub]
+@[to_additive (attr := push) zsmul_sub]
 lemma div_zpow (a b : α) (n : ℤ) : (a / b) ^ n = a ^ n / b ^ n := by
   simp only [div_eq_mul_inv, mul_zpow, inv_zpow]
 
@@ -799,7 +799,7 @@ theorem leftInverse_inv_mul_mul_right (c : G) :
 @[to_additive (attr := simp) natAbs_nsmul_eq_zero]
 lemma pow_natAbs_eq_one : a ^ n.natAbs = 1 ↔ a ^ n = 1 := by cases n <;> simp
 
-@[to_additive sub_nsmul]
+@[to_additive (attr := push) sub_nsmul]
 lemma pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ :=
   eq_mul_inv_of_mul_eq <| by rw [← pow_add, Nat.sub_add_cancel h]
 

Mathlib/Algebra/Group/Defs.lean

@@ -10,6 +10,7 @@ import Mathlib.Algebra.Group.Operations
 import Mathlib.Logic.Function.Defs
 import Mathlib.Tactic.Simps.Basic
 import Mathlib.Tactic.OfNat
+import Mathlib.Tactic.Push.Attr
 import Batteries.Logic
 
 /-!
@@ -597,7 +598,7 @@ lemma pow_three' (a : M) : a ^ 3 = a * a * a := by rw [pow_succ, pow_two]
 lemma pow_three (a : M) : a ^ 3 = a * (a * a) := by rw [pow_succ', pow_two]
 
 -- the attributes are intentionally out of order.
-@[to_additive nsmul_zero, simp] lemma one_pow : ∀ n, (1 : M) ^ n = 1
+@[to_additive (attr := push) nsmul_zero, simp] lemma one_pow : ∀ n, (1 : M) ^ n = 1
   | 0 => pow_zero _
   | n + 1 => by rw [pow_succ, one_pow, one_mul]
 
@@ -609,7 +610,8 @@ lemma pow_add (a : M) (m : ℕ) : ∀ n, a ^ (m + n) = a ^ m * a ^ n
 @[to_additive] lemma pow_mul_comm (a : M) (m n : ℕ) : a ^ m * a ^ n = a ^ n * a ^ m := by
   rw [← pow_add, ← pow_add, Nat.add_comm]
 
-@[to_additive mul_nsmul] lemma pow_mul (a : M) (m : ℕ) : ∀ n, a ^ (m * n) = (a ^ m) ^ n
+@[to_additive (attr := push ←) mul_nsmul]
+lemma pow_mul (a : M) (m : ℕ) : ∀ n, a ^ (m * n) = (a ^ m) ^ n
   | 0 => by rw [Nat.mul_zero, pow_zero, pow_zero]
   | n + 1 => by rw [Nat.mul_succ, pow_add, pow_succ, pow_mul]
 
@@ -727,7 +729,7 @@ class InvolutiveInv (G : Type*) extends Inv G where
 
 variable [InvolutiveInv G]
 
-@[to_additive (attr := simp)]
+@[to_additive (attr := simp, push)]
 theorem inv_inv (a : G) : a⁻¹⁻¹ = a :=
   InvolutiveInv.inv_inv _
 
@@ -981,7 +983,7 @@ section DivisionMonoid
 
 variable [DivisionMonoid G] {a b : G}
 
-@[to_additive (attr := simp) neg_add_rev]
+@[to_additive (attr := simp, push) neg_add_rev]
 theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
   DivisionMonoid.mul_inv_rev _ _
 

Mathlib/Algebra/Group/Pi/Basic.lean

@@ -50,7 +50,7 @@ instance instOne [∀ i, One <| f i] : One (∀ i : I, f i) :=
 theorem one_apply [∀ i, One <| f i] : (1 : ∀ i, f i) i = 1 :=
   rfl
 
-@[to_additive]
+@[to_additive (attr := push ←)]
 theorem one_def [∀ i, One <| f i] : (1 : ∀ i, f i) = fun _ => 1 :=
   rfl
 
@@ -72,7 +72,7 @@ instance instMul [∀ i, Mul <| f i] : Mul (∀ i : I, f i) :=
 theorem mul_apply [∀ i, Mul <| f i] : (x * y) i = x i * y i :=
   rfl
 
-@[to_additive]
+@[to_additive (attr := push ←)]
 theorem mul_def [∀ i, Mul <| f i] : x * y = fun i => x i * y i :=
   rfl
 
@@ -95,7 +95,7 @@ instance instPow [∀ i, Pow (f i) β] : Pow (∀ i, f i) β :=
 theorem pow_apply [∀ i, Pow (f i) β] (x : ∀ i, f i) (b : β) (i : I) : (x ^ b) i = x i ^ b :=
   rfl
 
-@[to_additive (attr := to_additive) (reorder := 5 6) smul_def]
+@[to_additive (attr := push ←, to_additive) (reorder := 5 6) smul_def]
 theorem pow_def [∀ i, Pow (f i) β] (x : ∀ i, f i) (b : β) : x ^ b = fun i => x i ^ b :=
   rfl
 
@@ -116,7 +116,7 @@ instance instInv [∀ i, Inv <| f i] : Inv (∀ i : I, f i) :=
 theorem inv_apply [∀ i, Inv <| f i] : x⁻¹ i = (x i)⁻¹ :=
   rfl
 
-@[to_additive]
+@[to_additive (attr := push ←)]
 theorem inv_def [∀ i, Inv <| f i] : x⁻¹ = fun i => (x i)⁻¹ :=
   rfl
 
@@ -135,7 +135,7 @@ instance instDiv [∀ i, Div <| f i] : Div (∀ i : I, f i) :=
 theorem div_apply [∀ i, Div <| f i] : (x / y) i = x i / y i :=
   rfl
 
-@[to_additive]
+@[to_additive (attr := push ←)]
 theorem div_def [∀ i, Div <| f i] : x / y = fun i => x i / y i :=
   rfl
 

Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

@@ -1008,12 +1008,8 @@ set_option push_neg.use_distrib true in
   constructor
   · contrapose!
     rintro (hs | rfl)
-    -- TODO: The `nonempty_iff_ne_empty` would be unnecessary if `push_neg` knew how to simplify
-    -- `s ≠ ∅` to `s.Nonempty` when `s : Finset α`.
-    -- See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/push_neg.20extensibility
-    · exact nonempty_iff_ne_empty.1 (nonempty_iff_ne_empty.2 hs).pow
-    · rw [← nonempty_iff_ne_empty]
-      simp
+    · exact hs.pow
+    · simp
   · rintro ⟨rfl, hn⟩
     exact empty_pow hn
 
@@ -1168,9 +1164,8 @@ set_option push_neg.use_distrib true in
   constructor
   · contrapose!
     rintro (hs | rfl)
-    · exact nonempty_iff_ne_empty.1 (nonempty_iff_ne_empty.2 hs).zpow
-    · rw [← nonempty_iff_ne_empty]
-      simp
+    · exact hs.zpow
+    · simp
   · rintro ⟨rfl, hn⟩
     exact empty_zpow hn
 

Mathlib/Algebra/GroupWithZero/Action/Defs.lean

@@ -313,7 +313,7 @@ theorem MulDistribMulAction.toMonoidHom_apply (r : M) (x : A) :
     MulDistribMulAction.toMonoidHom A r x = r • x :=
   rfl
 
-@[simp] lemma smul_pow' (r : M) (x : A) (n : ℕ) : r • x ^ n = (r • x) ^ n :=
+@[simp, push ←] lemma smul_pow' (r : M) (x : A) (n : ℕ) : r • x ^ n = (r • x) ^ n :=
   (MulDistribMulAction.toMonoidHom _ _).map_pow _ _
 
 end

Mathlib/Algebra/Lie/Submodule.lean

@@ -670,9 +670,10 @@ instance [Nontrivial M] : Nontrivial (LieSubmodule R L M) :=
 theorem nontrivial_iff_ne_bot {N : LieSubmodule R L M} : Nontrivial N ↔ N ≠ ⊥ := by
   constructor <;> contrapose!
   · rintro rfl
-      ⟨⟨m₁, h₁ : m₁ ∈ (⊥ : LieSubmodule R L M)⟩, ⟨m₂, h₂ : m₂ ∈ (⊥ : LieSubmodule R L M)⟩, h₁₂⟩
-    simp [(LieSubmodule.mem_bot _).mp h₁, (LieSubmodule.mem_bot _).mp h₂] at h₁₂
-  · rw [not_nontrivial_iff_subsingleton, LieSubmodule.eq_bot_iff]
+    constructor
+    rintro ⟨m₁, h₁ : m₁ ∈ (⊥ : LieSubmodule R L M)⟩ ⟨m₂, h₂ : m₂ ∈ (⊥ : LieSubmodule R L M)⟩
+    simp only [(LieSubmodule.mem_bot _).mp h₁, (LieSubmodule.mem_bot _).mp h₂]
+  · rw [LieSubmodule.eq_bot_iff]
     rintro ⟨h⟩ m hm
     simpa using h ⟨m, hm⟩ ⟨_, N.zero_mem⟩
 

Mathlib/Algebra/Lie/Weights/Linear.lean

@@ -248,8 +248,7 @@ lemma exists_nontrivial_weightSpace_of_isNilpotent [Field k] [LieAlgebra k L] [M
     [IsTriangularizable k L M] [Nontrivial M] :
     ∃ χ : Module.Dual k L, Nontrivial (weightSpace M χ) := by
   obtain ⟨χ⟩ : Nonempty (Weight k L M) := by
-    by_contra contra
-    rw [not_nonempty_iff] at contra
+    by_contra! contra
     simpa only [iSup_of_empty, bot_ne_top] using LieModule.iSup_genWeightSpace_eq_top' k L M
   obtain ⟨m, hm₀, hm⟩ := exists_forall_lie_eq_smul k L M χ
   simp only [LieSubmodule.nontrivial_iff_ne_bot, LieSubmodule.eq_bot_iff, Weight.coe_coe, ne_eq,

Mathlib/Algebra/Module/DedekindDomain.lean

@@ -64,7 +64,7 @@ theorem isInternal_prime_power_torsion [DecidableEq (Ideal R)] [Module.Finite R
   have hM' := Module.isTorsionBySet_annihilator_top R M
   have hI := Submodule.annihilator_top_inter_nonZeroDivisors hM
   refine isInternal_prime_power_torsion_of_is_torsion_by_ideal ?_ hM'
-  rw [← Set.nonempty_iff_ne_empty] at hI; rw [Submodule.ne_bot_iff]
+  push_neg at hI; rw [Submodule.ne_bot_iff]
   obtain ⟨x, H, hx⟩ := hI; exact ⟨x, H, nonZeroDivisors.ne_zero hx⟩
 
 /-- A finitely generated torsion module over a Dedekind domain is an internal direct sum of its

Mathlib/Algebra/Order/Antidiag/Nat.lean

@@ -74,7 +74,7 @@ theorem mem_finMulAntidiag {d n : ℕ} {f : Fin d → ℕ} :
       refine ⟨fun i ↦ ⟨f i, ?_⟩, rfl, funext fun _ => rfl⟩
       apply Nat.pos_of_ne_zero
       exact Finset.prod_ne_zero_iff.mp h.ne.symm _ (mem_univ _)
-  · simp only [not_lt, nonpos_iff_eq_zero] at h
+  · push_neg at h
     simp only [h, not_mem_empty, ne_eq, not_true_eq_false, and_false]
 
 @[simp]