chore(data/set/basic): Make set.nonempty.ne_empty an alias (#17382)

Make `nonempty.ne_empty` an alias of `ne_empty_iff_nonempty` and remove `empty_not_nonempty` in favor of `not_nonempty_empty`.

src/analysis/convex/exposed.lean

@@ -138,7 +138,7 @@ begin
   refine finset.induction _ _,
   { rintro h,
     exfalso,
-    exact empty_not_nonempty h },
+    exact not_nonempty_empty h },
   rintro C F _ hF _ hCF,
   rw [finset.coe_insert, sInter_insert],
   obtain rfl | hFnemp := F.eq_empty_or_nonempty,

src/data/set/basic.lean

@@ -298,13 +298,6 @@ lemma nonempty_of_mem {x} (h : x ∈ s) : s.nonempty := ⟨x, h⟩
 theorem nonempty.not_subset_empty : s.nonempty → ¬(s ⊆ ∅)
 | ⟨x, hx⟩ hs := hs hx
 
-/-- See also `set.ne_empty_iff_nonempty` and `set.not_nonempty_iff_eq_empty`. -/
-theorem nonempty.ne_empty : ∀ {s : set α}, s.nonempty → s ≠ ∅
-| _ ⟨x, hx⟩ rfl := hx
-
-@[simp] theorem not_nonempty_empty : ¬(∅ : set α).nonempty :=
-λ h, h.ne_empty rfl
-
 /-- Extract a witness from `s.nonempty`. This function might be used instead of case analysis
 on the argument. Note that it makes a proof depend on the `classical.choice` axiom. -/
 protected noncomputable def nonempty.some (h : s.nonempty) : α := classical.some h
@@ -381,13 +374,17 @@ eq_empty_of_subset_empty $ λ x hx, is_empty_elim x
 instance unique_empty [is_empty α] : unique (set α) :=
 { default := ∅, uniq := eq_empty_of_is_empty }
 
+/-- See also `set.ne_empty_iff_nonempty`. -/
 lemma not_nonempty_iff_eq_empty {s : set α} : ¬s.nonempty ↔ s = ∅ :=
 by simp only [set.nonempty, eq_empty_iff_forall_not_mem, not_exists]
 
-lemma empty_not_nonempty : ¬(∅ : set α).nonempty := λ h, h.ne_empty rfl
-
+/-- See also `set.not_nonempty_iff_eq_empty`. -/
 theorem ne_empty_iff_nonempty : s ≠ ∅ ↔ s.nonempty := not_iff_comm.1 not_nonempty_iff_eq_empty
 
+alias ne_empty_iff_nonempty ↔ _ nonempty.ne_empty
+
+@[simp] lemma not_nonempty_empty : ¬(∅ : set α).nonempty := λ ⟨x, hx⟩, hx
+
 @[simp] lemma is_empty_coe_sort {s : set α} : is_empty ↥s ↔ s = ∅ :=
 not_iff_not.1 $ by simpa using ne_empty_iff_nonempty.symm
 

src/data/set/finite.lean

@@ -1090,7 +1090,7 @@ lemma finite.exists_maximal_wrt [partial_order β] (f : α → β) (s : set α)
   s.nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a' :=
 begin
   refine h.induction_on _ _,
-  { exact λ h, absurd h empty_not_nonempty },
+  { exact λ h, absurd h not_nonempty_empty },
   intros a s his _ ih _,
   cases s.eq_empty_or_nonempty with h h,
   { use a, simp [h] },

src/measure_theory/measure/outer_measure.lean

@@ -53,7 +53,7 @@ outer measure, Carathéodory-measurable, Carathéodory's criterion
 
 noncomputable theory
 
-open set finset function filter topological_space (second_countable_topology)
+open set function filter topological_space (second_countable_topology)
 open_locale classical big_operators nnreal topological_space ennreal measure_theory
 
 namespace measure_theory
@@ -669,7 +669,7 @@ variables {α : Type*} (m : set α → ℝ≥0∞)
   satisfying `μ s ≤ m s` for all `s : set α`. This is the same as `outer_measure.of_function`,
   except that it doesn't require `m ∅ = 0`. -/
 def bounded_by : outer_measure α :=
-outer_measure.of_function (λ s, ⨆ (h : s.nonempty), m s) (by simp [empty_not_nonempty])
+outer_measure.of_function (λ s, ⨆ (h : s.nonempty), m s) (by simp [not_nonempty_empty])
 
 variables {m}
 theorem bounded_by_le (s : set α) : bounded_by m s ≤ m s :=
@@ -679,7 +679,7 @@ theorem bounded_by_eq_of_function (m_empty : m ∅ = 0) (s : set α) :
   bounded_by m s = outer_measure.of_function m m_empty s :=
 begin
   have : (λ s : set α, ⨆ (h : s.nonempty), m s) = m,
-  { ext1 t, cases t.eq_empty_or_nonempty with h h; simp [h, empty_not_nonempty, m_empty] },
+  { ext1 t, cases t.eq_empty_or_nonempty with h h; simp [h, not_nonempty_empty, m_empty] },
   simp [bounded_by, this]
 end
 theorem bounded_by_apply (s : set α) :
@@ -696,7 +696,7 @@ ext $ λ s, bounded_by_eq _ m.empty' (λ t ht, m.mono' ht) m.Union
 theorem le_bounded_by {μ : outer_measure α} : μ ≤ bounded_by m ↔ ∀ s, μ s ≤ m s :=
 begin
   rw [bounded_by, le_of_function, forall_congr], intro s,
-  cases s.eq_empty_or_nonempty with h h; simp [h, empty_not_nonempty]
+  cases s.eq_empty_or_nonempty with h h; simp [h, not_nonempty_empty]
 end
 
 theorem le_bounded_by' {μ : outer_measure α} :
@@ -874,7 +874,7 @@ lemma bounded_by_caratheodory {m : set α → ℝ≥0∞} {s : set α}
 begin
   apply of_function_caratheodory, intro t,
   cases t.eq_empty_or_nonempty with h h,
-  { simp [h, empty_not_nonempty] },
+  { simp [h, not_nonempty_empty] },
   { convert le_trans _ (hs t), { simp [h] }, exact add_le_add supr_const_le supr_const_le }
 end
 
@@ -932,7 +932,7 @@ lemma supr_Inf_gen_nonempty {m : set (outer_measure α)} (h : m.nonempty) (t : s
 begin
   rcases t.eq_empty_or_nonempty with rfl|ht,
   { rcases h with ⟨μ, hμ⟩,
-    rw [eq_false_intro empty_not_nonempty, supr_false, eq_comm],
+    rw [eq_false_intro not_nonempty_empty, supr_false, eq_comm],
     simp_rw [empty'],
     apply bot_unique,
     refine infi_le_of_le μ (infi_le _ hμ) },

src/order/filter/bases.lean

@@ -600,7 +600,7 @@ lemma mem_iff_inf_principal_compl {f : filter α} {s : set α} :
   s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥ :=
 begin
   refine not_iff_not.1 ((inf_principal_ne_bot_iff.trans _).symm.trans ne_bot_iff),
-  exact ⟨λ h hs, by simpa [empty_not_nonempty] using h s hs,
+  exact ⟨λ h hs, by simpa [not_nonempty_empty] using h s hs,
     λ hs t ht, inter_compl_nonempty_iff.2 $ λ hts, hs $ mem_of_superset ht hts⟩,
 end
 

src/order/filter/basic.lean

@@ -673,7 +673,7 @@ end
 
 lemma forall_mem_nonempty_iff_ne_bot {f : filter α} :
   (∀ (s : set α), s ∈ f → s.nonempty) ↔ ne_bot f :=
-⟨λ h, ⟨λ hf, empty_not_nonempty (h ∅ $ hf.symm ▸ mem_bot)⟩, @nonempty_of_mem _ _⟩
+⟨λ h, ⟨λ hf, not_nonempty_empty (h ∅ $ hf.symm ▸ mem_bot)⟩, @nonempty_of_mem _ _⟩
 
 instance [nonempty α] : nontrivial (filter α) :=
 ⟨⟨⊤, ⊥, ne_bot.ne $ forall_mem_nonempty_iff_ne_bot.1 $ λ s hs,