feat(Data/Finset/Empty): add @[push] tags for pushing negation (leanprover-community#32195)

JovanGerb · JovanGerb · commit fe7877b4f9aa · 2025-12-05T18:16:07.000Z
This PR tags `Finset.nonempty_iff_ne_empty` and `Finset.not_nonempty_iff_eq_empty` with `@[push]`, so that they can be used in `push_neg`, `by_cases!`, etc.

A bunch of proofs have been golfed using this.
diff --git a/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean b/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@@ -858,12 +858,8 @@ lemma Nonempty.pow (hs : s.Nonempty) : ∀ {n}, (s ^ n).Nonempty
   constructor
   · contrapose! +distrib
     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
 
@@ -1010,9 +1006,8 @@ lemma Nonempty.zpow (hs : s.Nonempty) : ∀ {n : ℤ}, (s ^ n).Nonempty
   constructor
   · contrapose! +distrib
     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
 
diff --git a/Mathlib/Algebra/Module/ZLattice/Basic.lean b/Mathlib/Algebra/Module/ZLattice/Basic.lean
@@ -562,12 +562,10 @@ theorem ZLattice.rank [hs : IsZLattice K L] : finrank ℤ L = finrank K E := by
     -- Since `finrank ℤ L > finrank K E`, there exists a vector `v ∈ b` with `v ∉ e`
     obtain ⟨v, hv⟩ : (Set.range b \ Set.range e).Nonempty := by
       rw [Basis.coe_mk, Subtype.range_coe_subtype, Set.setOf_mem_eq, ← Set.toFinset_nonempty]
-      contrapose h
-      rw [Finset.not_nonempty_iff_eq_empty, Set.toFinset_diff,
-        Finset.sdiff_eq_empty_iff_subset] at h
+      contrapose! h
+      rw [Set.toFinset_diff, Finset.sdiff_eq_empty_iff_subset] at h
       replace h := Finset.card_le_card h
-      rwa [not_lt, h_card, ← topEquiv.finrank_eq, ← h_spanE, ← ht_span,
-        finrank_span_set_eq_card ht_lin]
+      rwa [h_card, ← topEquiv.finrank_eq, ← h_spanE, ← ht_span, finrank_span_set_eq_card ht_lin]
     -- Assume that `e ∪ {v}` is not `ℤ`-linear independent then we get the contradiction
     suffices ¬ LinearIndepOn ℤ id (insert v (Set.range e)) by
       contrapose! this
diff --git a/Mathlib/Algebra/MonoidAlgebra/Degree.lean b/Mathlib/Algebra/MonoidAlgebra/Degree.lean
@@ -434,11 +434,11 @@ lemma supDegree_leadingCoeff_sum_eq
     (∑ j ∈ s, f j).leadingCoeff D = (f i).leadingCoeff D := by
   classical
   rw [← s.add_sum_erase _ hi]
-  by_cases hs : s.erase i = ∅
+  by_cases! hs : s.erase i = ∅
   · rw [hs, Finset.sum_empty, add_zero]; exact ⟨rfl, rfl⟩
   suffices _ from ⟨supDegree_add_eq_left this, leadingCoeff_add_eq_left this⟩
   refine supDegree_sum_lt ?_ (fun j hj => ?_)
-  · rw [Finset.nonempty_iff_ne_empty]; exact hs
+  · exact hs
   · rw [Finset.mem_erase] at hj; exact hmax j hj.2 hj.1
 
 open Finset in
diff --git a/Mathlib/Algebra/Order/Module/HahnEmbedding.lean b/Mathlib/Algebra/Order/Module/HahnEmbedding.lean
@@ -139,7 +139,7 @@ theorem iSupIndep_stratum : iSupIndep u.stratum := by
   obtain hf' := congrArg ArchimedeanClass.mk hf
   contrapose! hf' with h0
   rw [← hab, DFinsupp.sum]
-  by_cases hnonempty : f.support.Nonempty
+  by_cases! hnonempty : f.support.Nonempty
   · have hmem (x : ArchimedeanClass M) : (f x).val ∈ u.stratum x :=
       Set.mem_of_mem_of_subset (f x).prop (by simp)
     have hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk (f i).val) f.support := by
@@ -156,7 +156,7 @@ theorem iSupIndep_stratum : iSupIndep u.stratum := by
     contrapose! h
     rw [DFinsupp.notMem_support_iff, u.archimedeanClassMk_of_mem_stratum ha h0]
     simpa using (f c).prop
-  · rw [Finset.not_nonempty_iff_eq_empty.mp hnonempty]
+  · rw [hnonempty]
     symm
     simpa using h0
 
@@ -293,7 +293,7 @@ theorem baseEmbedding_pos {x : seed.baseEmbedding.domain} (hx : 0 < x) :
     contrapose! hne with hempty
     apply DFinsupp.sum_eq_zero
     intro c
-    simpa using DFinsupp.notMem_support_iff.mp (forall_not_of_not_exists hempty c)
+    simpa using DFinsupp.notMem_support_iff.mp (Finset.eq_empty_iff_forall_notMem.mp hempty c)
   have htop : f.support.min' hsupport ≠ ⊤ := by
     by_contra! h
     have h : ⊤ ∈ f.support := h ▸ f.support.min'_mem hsupport
@@ -338,16 +338,14 @@ theorem baseEmbedding_pos {x : seed.baseEmbedding.domain} (hx : 0 < x) :
   rw [DFinsupp.sum, mk_sum hsupport hmono]
   rw [seed.archimedeanClassMk_of_mem_stratum (f _).prop
     (by simpa using f.support.min'_mem hsupport)]
-  by_cases hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty
+  by_cases! hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty
   · rw [mk_sum hsupport' (hmono.mono (by simp))]
     rw [seed.archimedeanClassMk_of_mem_stratum (f _).prop (by
       simpa using (Finset.mem_erase.mp <| (f.support.erase _).min'_mem hsupport').2)]
     apply Finset.min'_lt_of_mem_erase_min'
     apply Finset.min'_mem _ _
   · -- special case: `f` has a single term, and becomes 0 after removing it
-    have : f.support.erase (f.support.min' hsupport) = ∅ :=
-      Finset.not_nonempty_iff_eq_empty.mp hsupport'
-    simpa [this] using lt_top_iff_ne_top.mpr htop
+    simpa [hsupport'] using lt_top_iff_ne_top.mpr htop
 
 theorem baseEmbedding_strictMono [IsOrderedAddMonoid R] : StrictMono seed.baseEmbedding := by
   intro x y h
diff --git a/Mathlib/Algebra/Polynomial/Basic.lean b/Mathlib/Algebra/Polynomial/Basic.lean
@@ -1053,7 +1053,6 @@ theorem coeffs_empty_iff {p : R[X]} : coeffs p = ∅ ↔ p = 0 := by
   rw [← support_nonempty] at h
   obtain ⟨n, hn⟩ := h
   rw [mem_support_iff] at hn
-  rw [← nonempty_iff_ne_empty]
   exact ⟨p.coeff n, coeff_mem_coeffs hn⟩
 
 @[simp]
diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -82,7 +82,7 @@ instance : Membership (Finset E) (SimplicialComplex 𝕜 E) :=
   ⟨fun K s => s ∈ K.faces⟩
 
 lemma nonempty_of_mem_faces (hs : s ∈ K.faces) : s.Nonempty := by
-  rw [Finset.nonempty_iff_ne_empty]; rintro rfl; exact K.empty_notMem hs
+  by_contra! rfl; exact K.empty_notMem hs
 
 /-- The underlying space of a simplicial complex is the union of its faces. -/
 def space (K : SimplicialComplex 𝕜 E) : Set E :=
diff --git a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
@@ -499,7 +499,7 @@ theorem WithSeminorms.isVonNBounded_iff_seminorm_bounded {s : Set E} (hp : WithS
     convert hI {i}
     rw [Finset.sup_singleton]
   intro hi I
-  by_cases hI : I.Nonempty
+  by_cases! hI : I.Nonempty
   · choose r hr h using hi
     have h' : 0 < I.sup' hI r := by
       rcases hI with ⟨i, hi⟩
@@ -508,7 +508,7 @@ theorem WithSeminorms.isVonNBounded_iff_seminorm_bounded {s : Set E} (hp : WithS
     refine lt_of_lt_of_le (h i x hx) ?_
     simp only [Finset.le_sup'_iff]
     exact ⟨i, hi, (Eq.refl _).le⟩
-  simp only [Finset.not_nonempty_iff_eq_empty.mp hI, Finset.sup_empty, coe_bot, Pi.zero_apply]
+  simp only [hI, Finset.sup_empty, coe_bot, Pi.zero_apply]
   exact ⟨1, zero_lt_one, fun _ _ => zero_lt_one⟩
 
 theorem WithSeminorms.image_isVonNBounded_iff_seminorm_bounded (f : G → E) {s : Set G}
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean b/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
@@ -164,11 +164,10 @@ just two summands. -/
 theorem posLog_sum {α : Type*} (s : Finset α) (f : α → ℝ) :
     log⁺ (∑ t ∈ s, f t) ≤ log (s.card) + ∑ t ∈ s, log⁺ (f t) := by
   -- Trivial case: empty sum
-  by_cases hs : s = ∅
+  by_cases! hs : s = ∅
   · simp [hs, posLog]
   -- Nontrivial case: Obtain maximal element…
-  obtain ⟨t_max, ht_max⟩ := s.exists_max_image (fun t ↦ |f t|)
-    (Finset.nonempty_iff_ne_empty.mpr hs)
+  obtain ⟨t_max, ht_max⟩ := s.exists_max_image (fun t ↦ |f t|) hs
   -- …then calculate
   calc log⁺ (∑ t ∈ s, f t)
   _ = log⁺ |∑ t ∈ s, f t| := by
diff --git a/Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean b/Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean
@@ -72,8 +72,9 @@ namespace IsApproximateSubgroup
 @[to_additive one_le]
 lemma one_le (hA : IsApproximateSubgroup K A) : 1 ≤ K := by
   obtain ⟨F, hF, hSF⟩ := hA.sq_covBySMul
-  have hF₀ : F ≠ ∅ := by rintro rfl; simp [hA.nonempty.pow.ne_empty] at hSF
-  exact hF.trans' <| by simpa [Finset.nonempty_iff_ne_empty]
+  grw [← hF]
+  have : F.Nonempty := by by_contra! rfl; simp [hA.nonempty.ne_empty] at hSF
+  simpa
 
 @[to_additive]
 lemma mono (hKL : K ≤ L) (hA : IsApproximateSubgroup K A) : IsApproximateSubgroup L A where
diff --git a/Mathlib/Combinatorics/Additive/Energy.lean b/Mathlib/Combinatorics/Additive/Energy.lean
@@ -107,9 +107,7 @@ variable (s t)
 variable {s t}
 
 @[to_additive (attr := simp)] lemma mulEnergy_pos_iff : 0 < Eₘ[s, t] ↔ s.Nonempty ∧ t.Nonempty where
-  mp h := of_not_not fun H => by
-    simp_rw [not_and_or, not_nonempty_iff_eq_empty] at H
-    obtain rfl | rfl := H <;> simp at h
+  mp h := by by_contra! +distrib rfl | rfl <;> simp at h
   mpr h := mulEnergy_pos h.1 h.2
 
 @[to_additive (attr := simp)] lemma mulEnergy_eq_zero_iff : Eₘ[s, t] = 0 ↔ s = ∅ ∨ t = ∅ := by
diff --git a/Mathlib/Combinatorics/Additive/VerySmallDoubling.lean b/Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
@@ -146,8 +146,7 @@ private lemma weaken_doubling (h : #(A * A) < (3 / 2 : ℚ) * #A) : #(A * A) < 2
   linarith only [h]
 
 private lemma nonempty_of_doubling (h : #(A * A) < (3 / 2 : ℚ) * #A) : A.Nonempty := by
-  rw [nonempty_iff_ne_empty]
-  rintro rfl
+  by_contra! rfl
   simp at h
 
 /-- If `A` has doubling strictly less than `3 / 2`, then `A⁻¹ * A` is a subgroup.
@@ -528,7 +527,7 @@ private lemma mul_card_le_expansion (hS : S.Nonempty) : (1 - K) * #A ≤ expansi
 
 @[simp] private lemma expansion_pos_iff (hK : K < 1) (hS : S.Nonempty) :
     0 < expansion K S A ↔ A.Nonempty where
-  mp hA := by rw [nonempty_iff_ne_empty]; rintro rfl; simp at hA
+  mp hA := by by_contra! rfl; simp at hA
   mpr := expansion_pos hK hS
 
 @[simp] private lemma expansion_smul_finset (K : ℝ) (S A : Finset G) (a : G) :
@@ -676,8 +675,7 @@ private lemma not_isFragment_empty (hK : K < 1) (hS : S.Nonempty) : ¬ IsFragmen
 
 private lemma IsFragment.nonempty (hK : K < 1) (hS : S.Nonempty) (hA : IsFragment K S A) :
     A.Nonempty := by
-  rw [nonempty_iff_ne_empty]
-  rintro rfl
+  by_contra! rfl
   simp [*, not_isFragment_empty hK hS] at hA
 
 private lemma IsAtom.nonempty (hK : K < 1) (hS : S.Nonempty) (hA : IsAtom K S A) : A.Nonempty :=
diff --git a/Mathlib/Combinatorics/Colex.lean b/Mathlib/Combinatorics/Colex.lean
@@ -480,7 +480,7 @@ def IsInitSeg (𝒜 : Finset (Finset α)) (r : ℕ) : Prop :=
 -/
 lemma IsInitSeg.total (h₁ : IsInitSeg 𝒜₁ r) (h₂ : IsInitSeg 𝒜₂ r) : 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁ := by
   classical
-  simp_rw [← sdiff_eq_empty_iff_subset, ← not_nonempty_iff_eq_empty]
+  simp_rw [← sdiff_eq_empty_iff_subset]
   by_contra! h
   have ⟨⟨s, hs⟩, t, ht⟩ := h
   rw [mem_sdiff] at hs ht
diff --git a/Mathlib/Combinatorics/Hall/Finite.lean b/Mathlib/Combinatorics/Hall/Finite.lean
@@ -56,7 +56,7 @@ theorem hall_cond_of_erase {x : ι} (a : α)
   haveI := Classical.decEq ι
   specialize ha (s'.image fun z => z.1)
   rw [image_nonempty, Finset.card_image_of_injective s' Subtype.coe_injective] at ha
-  by_cases he : s'.Nonempty
+  by_cases! he : s'.Nonempty
   · have ha' : #s' < #(s'.biUnion fun x => t x) := by
       convert ha he fun h => by simpa [← h] using mem_univ x using 2
       ext x
@@ -68,8 +68,7 @@ theorem hall_cond_of_erase {x : ι} (a : α)
       exact Nat.le_sub_one_of_lt ha'
     · rw [erase_eq_of_notMem hb]
       exact Nat.le_of_lt ha'
-  · rw [nonempty_iff_ne_empty, not_not] at he
-    subst s'
+  · subst s'
     simp
 
 /-- First case of the inductive step: assuming that
diff --git a/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean b/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
@@ -423,7 +423,7 @@ lemma supSum_of_univ_notMem (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜
   cases m
   · cases h𝒜₁.card_pos.ne hm
   obtain ⟨s, 𝒜, hs, rfl, rfl⟩ := card_eq_succ.1 hm.symm
-  have h𝒜 : 𝒜.Nonempty := nonempty_iff_ne_empty.2 (by rintro rfl; simp at h𝒜₃)
+  have h𝒜 : 𝒜.Nonempty := by by_contra! rfl; simp at h𝒜₃
   rw [insert_eq, eq_sub_of_add_eq (supSum_union_add_supSum_infs _ _), singleton_infs,
     supSum_singleton (ne_of_mem_of_not_mem (mem_insert_self _ _) h𝒜₂), ih, ih, add_sub_cancel_right]
   · exact card_image_le.trans_lt (lt_add_one _)
diff --git a/Mathlib/Combinatorics/SetFamily/KruskalKatona.lean b/Mathlib/Combinatorics/SetFamily/KruskalKatona.lean
@@ -209,9 +209,9 @@ private lemma familyMeasure_compression_lt_familyMeasure {U V : Finset (Fin n)}
   have uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜 :=
     filter_union_filter_neg_eq _ _
   have ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty := by
-    refine nonempty_iff_ne_empty.2 fun z ↦ a ?_
-    rw [filter_image, z, image_empty, union_empty]
-    rwa [z, union_empty] at uA
+    contrapose! a
+    rw [filter_image, a, image_empty, union_empty]
+    rwa [a, union_empty] at uA
   rw [familyMeasure, familyMeasure, sum_union compress_disjoint]
   conv_rhs => rw [← uA]
   rw [sum_union (disjoint_filter_filter_neg _ _ _), add_lt_add_iff_left, filter_image,
diff --git a/Mathlib/Combinatorics/SimpleGraph/Clique.lean b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
@@ -808,10 +808,10 @@ lemma IsIndepSet.nonempty_mem_compl_mem_edge
     [Fintype α] [DecidableEq α] {s : Finset α} (indA : G.IsIndepSet s) {e} (he : e ∈ G.edgeSet) :
     { b ∈ sᶜ | b ∈ e }.Nonempty := by
   obtain ⟨v, w⟩ := e
-  by_contra c
+  by_contra! c
   rw [IsIndepSet] at indA
   rw [mem_edgeSet] at he
-  rw [not_nonempty_iff_eq_empty, filter_eq_empty_iff] at c
+  rw [filter_eq_empty_iff] at c
   simp_rw [mem_compl, Sym2.mem_iff, not_or] at c
   by_cases vins : v ∈ s
   · have wins : w ∈ s := by by_contra wnins; exact (c wnins).right rfl
diff --git a/Mathlib/Data/Finset/BooleanAlgebra.lean b/Mathlib/Data/Finset/BooleanAlgebra.lean
@@ -53,7 +53,7 @@ theorem univ_nonempty [Nonempty α] : (univ : Finset α).Nonempty :=
   univ_nonempty_iff.2 ‹_›
 
 theorem univ_eq_empty_iff : (univ : Finset α) = ∅ ↔ IsEmpty α := by
-  rw [← not_nonempty_iff, ← univ_nonempty_iff, not_nonempty_iff_eq_empty]
+  contrapose!; exact univ_nonempty_iff
 
 theorem univ_nontrivial_iff :
     (Finset.univ : Finset α).Nontrivial ↔ Nontrivial α := by
diff --git a/Mathlib/Data/Finset/Card.lean b/Mathlib/Data/Finset/Card.lean
@@ -591,8 +591,9 @@ theorem card_sdiff_add_card (s t : Finset α) : #(s \ t) + #t = #(s ∪ t) := by
   rw [← card_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]
 
 theorem sdiff_nonempty_of_card_lt_card (h : #s < #t) : (t \ s).Nonempty := by
-  rw [nonempty_iff_ne_empty, Ne, sdiff_eq_empty_iff_subset]
-  exact fun h' ↦ h.not_ge (card_le_card h')
+  contrapose! h
+  rw [sdiff_eq_empty_iff_subset] at h
+  grw [h]
 
 omit [DecidableEq α] in
 theorem exists_mem_notMem_of_card_lt_card (h : #s < #t) : ∃ e, e ∈ t ∧ e ∉ s := by
@@ -626,7 +627,7 @@ theorem inter_nonempty_of_card_lt_card_add_card (hts : t ⊆ s) (hus : u ⊆ s)
     (hstu : #s < #t + #u) : (t ∩ u).Nonempty := by
   contrapose! hstu
   calc
-    _ = #(t ∪ u) := by simp [← card_union_add_card_inter, not_nonempty_iff_eq_empty.1 hstu]
+    _ = #(t ∪ u) := by simp [← card_union_add_card_inter, hstu]
     _ ≤ #s := by gcongr; exact union_subset hts hus
 
 end Lattice
diff --git a/Mathlib/Data/Finset/Empty.lean b/Mathlib/Data/Finset/Empty.lean
@@ -144,10 +144,11 @@ theorem not_ssubset_empty (s : Finset α) : ¬s ⊂ ∅ := by grind
 theorem nonempty_of_ne_empty {s : Finset α} (h : s ≠ ∅) : s.Nonempty :=
   exists_mem_of_ne_zero (mt val_eq_zero.1 h)
 
+@[push ←]
 theorem nonempty_iff_ne_empty {s : Finset α} : s.Nonempty ↔ s ≠ ∅ :=
   ⟨Nonempty.ne_empty, nonempty_of_ne_empty⟩
 
-@[simp]
+@[simp, push]
 theorem not_nonempty_iff_eq_empty {s : Finset α} : ¬s.Nonempty ↔ s = ∅ :=
   nonempty_iff_ne_empty.not.trans not_not
 
diff --git a/Mathlib/Data/Finset/Filter.lean b/Mathlib/Data/Finset/Filter.lean
@@ -217,8 +217,8 @@ lemma _root_.Set.pairwiseDisjoint_filter [DecidableEq β] (f : α → β) (s : S
 theorem disjoint_filter_and_not_filter :
     Disjoint (s.filter (fun x ↦ p x ∧ ¬q x)) (s.filter (fun x ↦ q x ∧ ¬p x)) := by
   intro _ htp htq
-  simp only [bot_eq_empty, le_eq_subset, subset_empty, ← not_nonempty_iff_eq_empty]
-  rintro ⟨_, hx⟩
+  simp only [bot_eq_empty, le_eq_subset, subset_empty]
+  by_contra! ⟨_, hx⟩
   exact (mem_filter.mp (htq hx)).2.2 (mem_filter.mp (htp hx)).2.1
 
 variable {p q}
diff --git a/Mathlib/Data/Finset/Max.lean b/Mathlib/Data/Finset/Max.lean
@@ -405,10 +405,10 @@ theorem min'_erase_ne_self {s : Finset α} (s0 : (s.erase x).Nonempty) : (s.eras
   ne_of_mem_erase (min'_mem _ s0)
 
 theorem max_erase_ne_self {s : Finset α} : (s.erase x).max ≠ x := by
-  by_cases s0 : (s.erase x).Nonempty
+  by_cases! s0 : (s.erase x).Nonempty
   · refine ne_of_eq_of_ne (coe_max' s0).symm ?_
     exact WithBot.coe_eq_coe.not.mpr (max'_erase_ne_self _)
-  · rw [not_nonempty_iff_eq_empty.mp s0, max_empty]
+  · rw [s0, max_empty]
     exact WithBot.bot_ne_coe
 
 theorem min_erase_ne_self {s : Finset α} : (s.erase x).min ≠ x := by
diff --git a/Mathlib/Data/Finset/NAry.lean b/Mathlib/Data/Finset/NAry.lean
@@ -129,7 +129,7 @@ theorem image₂_empty_right : image₂ f s ∅ = ∅ :=
 
 @[simp]
 theorem image₂_eq_empty_iff : image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅ := by
-  simp_rw [← not_nonempty_iff_eq_empty, image₂_nonempty_iff, not_and_or]
+  contrapose!; exact image₂_nonempty_iff
 
 @[simp]
 theorem image₂_singleton_left : image₂ f {a} t = t.image fun b => f a b :=
diff --git a/Mathlib/Data/Finset/Pi.lean b/Mathlib/Data/Finset/Pi.lean
@@ -100,7 +100,7 @@ alias ⟨_, pi_nonempty_of_forall_nonempty⟩ := pi_nonempty
 
 @[simp]
 lemma pi_eq_empty : s.pi t = ∅ ↔ ∃ a ∈ s, t a = ∅ := by
-  simp [← not_nonempty_iff_eq_empty]
+  contrapose!; exact pi_nonempty
 
 @[simp]
 theorem pi_insert [∀ a, DecidableEq (β a)] {s : Finset α} {t : ∀ a : α, Finset (β a)} {a : α}
diff --git a/Mathlib/Data/Finset/Powerset.lean b/Mathlib/Data/Finset/Powerset.lean
@@ -212,7 +212,7 @@ theorem powersetCard_one (s : Finset α) :
 lemma powersetCard_eq_empty : powersetCard n s = ∅ ↔ s.card < n := by
   refine ⟨?_, fun h ↦ card_eq_zero.1 <| by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]⟩
   contrapose!
-  exact fun h ↦ nonempty_iff_ne_empty.1 <| (exists_subset_card_eq h).imp <| by simp
+  exact fun h ↦ (exists_subset_card_eq h).imp <| by simp
 
 @[simp] lemma powersetCard_card_add (s : Finset α) (hn : 0 < n) :
     s.powersetCard (s.card + n) = ∅ := by simpa
diff --git a/Mathlib/Data/Finset/Prod.lean b/Mathlib/Data/Finset/Prod.lean
@@ -194,8 +194,7 @@ theorem nonempty_product : (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty :=
 
 @[simp]
 theorem product_eq_empty {s : Finset α} {t : Finset β} : s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅ := by
-  rw [← not_nonempty_iff_eq_empty, nonempty_product, not_and_or, not_nonempty_iff_eq_empty,
-    not_nonempty_iff_eq_empty]
+  contrapose!; exact nonempty_product
 
 @[simp]
 theorem singleton_product {a : α} :
@@ -270,8 +269,7 @@ theorem diag_nonempty : s.diag.Nonempty ↔ s.Nonempty := by
 
 @[simp, grind =]
 theorem diag_eq_empty : s.diag = ∅ ↔ s = ∅ := by
-  have := (diag_nonempty (s := s)).not
-  rwa [not_nonempty_iff_eq_empty, not_nonempty_iff_eq_empty] at this
+  contrapose!; exact diag_nonempty
 
 variable (s)
 
diff --git a/Mathlib/Data/Finset/Sigma.lean b/Mathlib/Data/Finset/Sigma.lean
@@ -64,7 +64,7 @@ alias ⟨_, Aesop.sigma_nonempty_of_exists_nonempty⟩ := sigma_nonempty
 
 @[simp]
 theorem sigma_eq_empty : s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅ := by
-  simp only [← not_nonempty_iff_eq_empty, sigma_nonempty, not_exists, not_and]
+  contrapose!; exact sigma_nonempty
 
 @[mono]
 theorem sigma_mono (hs : s₁ ⊆ s₂) (ht : ∀ i, t₁ i ⊆ t₂ i) : s₁.sigma t₁ ⊆ s₂.sigma t₂ :=
diff --git a/Mathlib/Data/Finset/Sym.lean b/Mathlib/Data/Finset/Sym.lean
diff --git a/Mathlib/Data/Finsupp/Defs.lean b/Mathlib/Data/Finsupp/Defs.lean
diff --git a/Mathlib/Data/Nat/PrimeFin.lean b/Mathlib/Data/Nat/PrimeFin.lean
diff --git a/Mathlib/GroupTheory/CosetCover.lean b/Mathlib/GroupTheory/CosetCover.lean
diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean
diff --git a/Mathlib/LinearAlgebra/RootSystem/Base.lean b/Mathlib/LinearAlgebra/RootSystem/Base.lean
diff --git a/Mathlib/MeasureTheory/SetAlgebra.lean b/Mathlib/MeasureTheory/SetAlgebra.lean
diff --git a/Mathlib/NumberTheory/Divisors.lean b/Mathlib/NumberTheory/Divisors.lean
diff --git a/Mathlib/Order/Interval/Finset/Basic.lean b/Mathlib/Order/Interval/Finset/Basic.lean
diff --git a/Mathlib/Order/Partition/Finpartition.lean b/Mathlib/Order/Partition/Finpartition.lean
diff --git a/Mathlib/RingTheory/HahnSeries/Multiplication.lean b/Mathlib/RingTheory/HahnSeries/Multiplication.lean
diff --git a/Mathlib/RingTheory/HahnSeries/Summable.lean b/Mathlib/RingTheory/HahnSeries/Summable.lean
diff --git a/Mathlib/Topology/EMetricSpace/PairReduction.lean b/Mathlib/Topology/EMetricSpace/PairReduction.lean
