chore(Order.Filter): remove duplicated lemmas (#6932)

Remove the lemmas `le_pure_iff_eq_pure` (duplicate of `NeBot.le_pure_iff`) and `eq_bot_or_pure_of_subsingleton_mem` (duplicate of `subsingleton_iff_bot_or_pure`). 

This requires moving a few lemmas after their non-duplicate prerequisites.

Author: sgouezel

Mathlib/Order/Filter/AtTopBot.lean

@@ -302,18 +302,6 @@ theorem OrderBot.atBot_eq (α) [PartialOrder α] [OrderBot α] : (atBot : Filter
   @OrderTop.atTop_eq αᵒᵈ _ _
 #align filter.order_bot.at_bot_eq Filter.OrderBot.atBot_eq
 
-lemma atTop_eq_pure_of_isTop [LinearOrder α] {x : α} (hx : IsTop x) :
-    (atTop : Filter α) = pure x := by
-  have : Nonempty α := ⟨x⟩
-  have : (atTop : Filter α).NeBot := atTop_basis.neBot_iff.2 (fun _ ↦ ⟨x, hx _⟩)
-  apply eq_pure_iff_singleton_mem.2
-  convert Ici_mem_atTop x using 1
-  exact (Ici_eq_singleton_iff_isTop.2 hx).symm
-
-lemma atBot_eq_pure_of_isBot [LinearOrder α] {x : α} (hx : IsBot x) :
-    (atBot : Filter α) = pure x :=
-  @atTop_eq_pure_of_isTop αᵒᵈ _ _ hx
-
 @[nontriviality]
 theorem Subsingleton.atTop_eq (α) [Subsingleton α] [Preorder α] : (atTop : Filter α) = ⊤ := by
   refine' top_unique fun s hs x => _

Mathlib/Order/Filter/Bases.lean

@@ -1192,12 +1192,6 @@ theorem isCountablyGenerated_top : IsCountablyGenerated (⊤ : Filter α) :=
   @principal_univ α ▸ isCountablyGenerated_principal _
 #align filter.is_countably_generated_top Filter.isCountablyGenerated_top
 
-lemma isCountablyGenerated_of_subsingleton_mem {l : Filter α} {s : Set α} (hs : s.Subsingleton)
-    (h's : s ∈ l) : IsCountablyGenerated l := by
-  rcases eq_bot_or_pure_of_subsingleton_mem hs h's with rfl|⟨x, rfl⟩
-  · exact isCountablyGenerated_bot
-  · exact isCountablyGenerated_pure x
-
 -- porting note: without explicit `Sort u` and `Type v`, Lean 4 uses `ι : Prop`
 universe u v
 

Mathlib/Order/Filter/Basic.lean

@@ -2681,31 +2681,6 @@ theorem le_pure_iff {f : Filter α} {a : α} : f ≤ pure a ↔ {a} ∈ f := by
   rw [← principal_singleton, le_principal_iff]
 #align filter.le_pure_iff Filter.le_pure_iff
 
-lemma le_pure_iff_eq_pure {l : Filter α} [hl : NeBot l] :
-    l ≤ pure x ↔ l = pure x := by
-  refine' ⟨fun h ↦ _, fun h ↦ h.le⟩
-  have hx := le_pure_iff.1 h
-  ext s
-  simp only [mem_pure]
-  refine ⟨fun h ↦ ?_, fun h ↦ mem_of_superset hx (singleton_subset_iff.2 h)⟩
-  by_contra H
-  have : s ∩ {x} ∈ l := inter_mem h hx
-  rw [inter_singleton_eq_empty.2 H, empty_mem_iff_bot] at this
-  exact NeBot.ne hl this
-
-lemma eq_pure_iff_singleton_mem {l : Filter α} [hl : NeBot l] {x : α} :
-    l = pure x ↔ {x} ∈ l := by
-  rw [← le_pure_iff_eq_pure, le_pure_iff]
-
-lemma eq_bot_or_pure_of_subsingleton_mem {l : Filter α} {s : Set α} (hs : s.Subsingleton)
-    (h's : s ∈ l) : l = ⊥ ∨ ∃ x, l = pure x := by
-  rcases l.eq_or_neBot with rfl|hl
-  · exact Or.inl rfl
-  · rcases hs.eq_empty_or_singleton with rfl|⟨x, rfl⟩
-    · rw [empty_mem_iff_bot.1 h's]
-      exact Or.inl rfl
-    · exact Or.inr ⟨x, eq_pure_iff_singleton_mem.2 h's⟩
-
 theorem mem_seq_def {f : Filter (α → β)} {g : Filter α} {s : Set β} :
     s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, ∀ x ∈ u, ∀ y ∈ t, (x : α → β) y ∈ s :=
   Iff.rfl

Mathlib/Order/Filter/Subsingleton.lean

@@ -72,3 +72,8 @@ theorem subsingleton_iff_exists_singleton_mem [Nonempty α] : l.Subsingleton ↔
 
 /-- A subsingleton filter on a nonempty type is less than or equal to `pure a` for some `a`. -/
 alias ⟨Subsingleton.exists_le_pure, _⟩ := subsingleton_iff_exists_le_pure
+
+lemma Subsingleton.isCountablyGenerated (hl : l.Subsingleton) : IsCountablyGenerated l := by
+  rcases subsingleton_iff_bot_or_pure.1 hl with rfl|⟨x, rfl⟩
+  · exact isCountablyGenerated_bot
+  · exact isCountablyGenerated_pure x

Mathlib/Order/Filter/Ultrafilter.lean

@@ -414,6 +414,21 @@ protected theorem NeBot.le_pure_iff (hf : f.NeBot) : f ≤ pure a ↔ f = pure a
   ⟨Ultrafilter.unique (pure a), le_of_eq⟩
 #align filter.ne_bot.le_pure_iff Filter.NeBot.le_pure_iff
 
+protected theorem NeBot.eq_pure_iff (hf : f.NeBot) {x : α} :
+    f = pure x ↔ {x} ∈ f := by
+  rw [← hf.le_pure_iff, le_pure_iff]
+
+lemma atTop_eq_pure_of_isTop [LinearOrder α] {x : α} (hx : IsTop x) :
+    (atTop : Filter α) = pure x := by
+  have : Nonempty α := ⟨x⟩
+  apply atTop_neBot.eq_pure_iff.2
+  convert Ici_mem_atTop x using 1
+  exact (Ici_eq_singleton_iff_isTop.2 hx).symm
+
+lemma atBot_eq_pure_of_isBot [LinearOrder α] {x : α} (hx : IsBot x) :
+    (atBot : Filter α) = pure x :=
+  @atTop_eq_pure_of_isTop αᵒᵈ _ _ hx
+
 @[simp]
 theorem lt_pure_iff : f < pure a ↔ f = ⊥ :=
   isAtom_pure.lt_iff