extract

Author: plp127

Mathlib/Order/Filter/Cofinite.lean

@@ -286,20 +286,27 @@ A filter is free iff it is smaller than the cofinite filter.
 -/
 theorem le_cofinite_iff_ker (f : Filter α) : f ≤ cofinite ↔ f.ker = ∅ := by
   rw [le_cofinite_iff_compl_singleton_mem, ker_def, iInter₂_eq_empty_iff]
-  refine forall_congr' fun x => ⟨fun h => ⟨{x}ᶜ, h, by simp⟩,
-    fun ⟨s, hs, hx⟩ => f.mem_of_superset hs (by simpa using hx)⟩
+  exact forall_congr' fun x => ⟨fun h => ⟨{x}ᶜ, h, by simp⟩,
+    fun ⟨s, hs, hx⟩ => mem_of_superset hs (by simpa using hx)⟩
+
+lemma eq_principal_ker_sup_inf_principal_ker_compl (f : Filter α) :
+    f = 𝓟 f.ker ⊔ (f ⊓ 𝓟 f.kerᶜ) := by
+  rw [sup_inf_left]
+  simpa using gi_principal_ker.gc.l_u_le f
+
+lemma inf_principal_ker_compl_le_cofinite (f : Filter α) : f ⊓ 𝓟 f.kerᶜ ≤ cofinite := by
+  rw [le_cofinite_iff_ker, ker_inf, ker_principal, inter_compl_self]
 
 /--
 Every filter is the disjoint supremum of a principal filter and a free filter in a unique way.
 -/
 theorem existsUnique_eq_principal_sup_free (f : Filter α) :
     ∃! p : Set α × Filter α, p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2 := by
   refine ⟨(f.ker, f ⊓ 𝓟 f.kerᶜ), ⟨?_, ?_, ?_⟩, fun q hq => ?_⟩
-  · rw [le_cofinite_iff_ker, ker_inf, ker_principal, inter_compl_self]
+  · exact inf_principal_ker_compl_le_cofinite f
   · rw [disjoint_principal_left]
     exact mem_inf_of_right (mem_principal_self f.kerᶜ)
-  · rw [sup_inf_left]
-    simpa using gi_principal_ker.gc.l_u_le f
+  · exact eq_principal_ker_sup_inf_principal_ker_compl f
   · have hqk := congrArg Filter.ker hq.2.2
     rw [ker_sup, ker_principal, (le_cofinite_iff_ker q.2).mp hq.1, union_empty] at hqk
     refine congrArg₂ Prod.mk hqk.symm (le_antisymm (le_inf ?_ ?_) ?_)