chore(data/{finset,set}/basic): Align lemmas (#17805)

Match the `set` and `finset` statements.



Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Author: YaelDillies

archive/imo/imo1988_q6.lean

@@ -111,8 +111,8 @@ begin
       -- And hence we are done by H_zero and H_diag.
       solve_by_elim } },
   -- To finish the main proof, we need to show that the exceptional locus is nonempty.
-  -- So we assume that the exceptional locus is empty, and work towards dering a contradiction.
-  rw ← set.ne_empty_iff_nonempty,
+  -- So we assume that the exceptional locus is empty, and work towards deriving a contradiction.
+  rw set.nonempty_iff_ne_empty,
   assume exceptional_empty,
   -- Observe that S is nonempty.
   have S_nonempty : S.nonempty,

counterexamples/phillips.lean

@@ -532,7 +532,7 @@ begin
     ⊆ ⋃ y ∈ φ.to_bounded_additive_measure.discrete_support, {x | y ∈ spf Hcont x},
   { assume x hx,
     dsimp at hx,
-    rw [← ne.def, ne_empty_iff_nonempty] at hx,
+    rw [← ne.def, ←nonempty_iff_ne_empty] at hx,
     simp only [exists_prop, mem_Union, mem_set_of_eq],
     exact hx },
   apply countable.mono (subset.trans A B),

src/algebra/big_operators/finprod.lean

@@ -540,7 +540,7 @@ lemma finprod_mem_empty : ∏ᶠ i ∈ (∅ : set α), f i = 1 := by simp
 /-- A set `s` is nonempty if the product of some function over `s` is not equal to `1`. -/
 @[to_additive "A set `s` is nonempty if the sum of some function over `s` is not equal to `0`."]
 lemma nonempty_of_finprod_mem_ne_one (h : ∏ᶠ i ∈ s, f i ≠ 1) : s.nonempty :=
-ne_empty_iff_nonempty.1 $ λ h', h $ h'.symm ▸ finprod_mem_empty
+nonempty_iff_ne_empty.2 $ λ h', h $ h'.symm ▸ finprod_mem_empty
 
 /-- Given finite sets `s` and `t`, the product of `f i` over `i ∈ s ∪ t` times the product of
 `f i` over `i ∈ s ∩ t` equals the product of `f i` over `i ∈ s` times the product of `f i`

src/algebra/lie/solvable.lean

@@ -333,8 +333,8 @@ lemma derived_length_zero (I : lie_ideal R L) [hI : is_solvable R I] :
 begin
   let s := {k | derived_series_of_ideal R L k I = ⊥}, change Inf s = 0 ↔ _,
   have hne : s ≠ ∅,
-  { rw set.ne_empty_iff_nonempty,
-    obtain ⟨k, hk⟩ := id hI, use k,
+  { obtain ⟨k, hk⟩ := id hI,
+    refine set.nonempty.ne_empty ⟨k, _⟩,
     rw [derived_series_def, lie_ideal.derived_series_eq_bot_iff] at hk, exact hk, },
   simp [hne],
 end

src/algebra/module/dedekind_domain.lean

@@ -62,7 +62,7 @@ theorem is_internal_prime_power_torsion [module.finite R M] (hM : module.is_tors
 begin
   obtain ⟨I, hI, hM'⟩ := is_torsion_by_ideal_of_finite_of_is_torsion hM,
   refine is_internal_prime_power_torsion_of_is_torsion_by_ideal _ hM',
-  rw set.ne_empty_iff_nonempty at hI, rw submodule.ne_bot_iff,
+  rw ←set.nonempty_iff_ne_empty at hI, rw submodule.ne_bot_iff,
   obtain ⟨x, H, hx⟩ := hI, exact ⟨x, H, non_zero_divisors.ne_zero hx⟩
 end
 

src/algebra/module/torsion.lean

@@ -501,8 +501,7 @@ lemma is_torsion_by_ideal_of_finite_of_is_torsion [module.finite R M] (hM : modu
 begin
   cases (module.finite_def.mp infer_instance : (⊤ : submodule R M).fg) with S h,
   refine ⟨∏ x in S, ideal.torsion_of R M x, _, _⟩,
-  { rw set.ne_empty_iff_nonempty,
-    refine ⟨_, _, (∏ x in S, (@hM x).some : R⁰).2⟩,
+  { refine set.nonempty.ne_empty ⟨_, _, (∏ x in S, (@hM x).some : R⁰).2⟩,
     rw [subtype.val_eq_coe, submonoid.coe_finset_prod],
     apply ideal.prod_mem_prod,
     exact λ x _, (@hM x).some_spec },

src/algebra/support.lean

@@ -76,7 +76,7 @@ by { simp_rw [← subset_empty_iff, mul_support_subset_iff', funext_iff], simp }
 
 @[simp, to_additive] lemma mul_support_nonempty_iff {f : α → M} :
   (mul_support f).nonempty ↔ f ≠ 1 :=
-by rw [← ne_empty_iff_nonempty, ne.def, mul_support_eq_empty_iff]
+by rw [nonempty_iff_ne_empty, ne.def, mul_support_eq_empty_iff]
 
 @[to_additive]
 lemma range_subset_insert_image_mul_support (f : α → M) :

src/algebraic_geometry/function_field.lean

@@ -54,7 +54,7 @@ begin
   replace ha := ne_of_apply_ne _ ha,
   have hs : generic_point X.carrier ∈ RingedSpace.basic_open _ s,
   { rw [← opens.mem_coe, (generic_point_spec X.carrier).mem_open_set_iff, set.top_eq_univ,
-      set.univ_inter, ← set.ne_empty_iff_nonempty, ne.def, ← opens.coe_bot,
+      set.univ_inter, set.nonempty_iff_ne_empty, ne.def, ← opens.coe_bot,
       subtype.coe_injective.eq_iff, ← opens.empty_eq],
     erw basic_open_eq_bot_iff,
     exacts [ha, (RingedSpace.basic_open _ _).prop] },

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -260,9 +260,8 @@ begin
   split,
   { contrapose!,
     intro h,
-    apply set.ne_empty_iff_nonempty.mpr,
     rcases ideal.exists_le_maximal I h with ⟨M, hM, hIM⟩,
-    exact ⟨⟨M, hM.is_prime⟩, hIM⟩ },
+    exact set.nonempty.ne_empty ⟨⟨M, hM.is_prime⟩, hIM⟩ },
   { rintro rfl, apply zero_locus_empty_of_one_mem, trivial }
 end
 
@@ -458,7 +457,7 @@ lemma is_irreducible_zero_locus_iff_of_radical (I : ideal R) (hI : I.is_radical)
 begin
   rw [ideal.is_prime_iff, is_irreducible],
   apply and_congr,
-  { rw [← set.ne_empty_iff_nonempty, ne.def, zero_locus_empty_iff_eq_top] },
+  { rw [set.nonempty_iff_ne_empty, ne.def, zero_locus_empty_iff_eq_top] },
   { transitivity ∀ (x y : ideal R), Z(I) ⊆ Z(x) ∪ Z(y) → Z(I) ⊆ Z(x) ∨ Z(I) ⊆ Z(y),
     { simp_rw [is_preirreducible_iff_closed_union_closed, is_closed_iff_zero_locus_ideal],
       split,

src/analysis/bounded_variation.lean

@@ -393,11 +393,11 @@ begin
   by_cases hs : s = ∅,
   { simp [hs] },
   haveI : nonempty {u // monotone u ∧ ∀ (i : ℕ), u i ∈ s},
-    from nonempty_monotone_mem (ne_empty_iff_nonempty.1 hs),
+    from nonempty_monotone_mem (nonempty_iff_ne_empty.2 hs),
   by_cases ht : t = ∅,
   { simp [ht] },
   haveI : nonempty {u // monotone u ∧ ∀ (i : ℕ), u i ∈ t},
-    from nonempty_monotone_mem (ne_empty_iff_nonempty.1 ht),
+    from nonempty_monotone_mem (nonempty_iff_ne_empty.2 ht),
   refine ennreal.supr_add_supr_le _,
   /- We start from two sequences `u` and `v` along `s` and `t` respectively, and we build a new
   sequence `w` along `s ∪ t` by juxtaposing them. Its variation is larger than the sum of the