chore(Order/Filter/CardinalInter): fix typos and polish docs (#31624)

Issues found and fixed with help from Codex.

Author: harahu

Mathlib/Order/Filter/CardinalInter.lean

@@ -25,7 +25,7 @@ their intersection belongs to `l` as well.
     `c > ℵ₀` is a `CountableInterFilter`.
 * `CountableInterFilter.toCardinalInterFilter` establishes that every `CountableInterFilter l` is a
     `CardinalInterFilter l ℵ₁`.
-* `CardinalInterFilter.of_CardinalInterFilter_of_lt` establishes that we have
+* `CardinalInterFilter.of_cardinalInterFilter_of_lt` establishes that we have
   `CardinalInterFilter l c` → `CardinalInterFilter l a` for all `a < c`.
 
 ## Tags
@@ -77,7 +77,7 @@ theorem cardinalInterFilter_aleph_one_iff :
     CardinalInterFilter.cardinal_sInter_mem S ((countable_iff_lt_aleph_one S).1 h) a⟩,
    fun _ ↦ CountableInterFilter.toCardinalInterFilter l⟩
 
-/-- Every CardinalInterFilter for some c also is a CardinalInterFilter for some a ≤ c -/
+/-- Every `CardinalInterFilter` for some `c` also is a `CardinalInterFilter` for any `a ≤ c`. -/
 theorem CardinalInterFilter.of_cardinalInterFilter_of_le (l : Filter α) [CardinalInterFilter l c]
     {a : Cardinal.{u}} (hac : a ≤ c) :
     CardinalInterFilter l a where
@@ -287,7 +287,8 @@ inductive CardinalGenerateSets : Set α → Prop
   | sInter {S : Set (Set α)} :
     (#S < c) → (∀ s ∈ S, CardinalGenerateSets s) → CardinalGenerateSets (⋂₀ S)
 
-/-- `Filter.cardinalGenerate c g` is the greatest `cardinalInterFilter c` containing `g`. -/
+/-- Assuming `2 < c`, `Filter.cardinalGenerate c g` is the greatest `CardinalInterFilter c`
+containing `g`. -/
 def cardinalGenerate (hc : 2 < c) : Filter α :=
   ofCardinalInter (CardinalGenerateSets g) hc (fun _ => CardinalGenerateSets.sInter) fun _ _ =>
     CardinalGenerateSets.superset
@@ -301,7 +302,7 @@ variable {g}
 
 /-- A set is in the `cardinalInterFilter` generated by `g` if and only if
 it contains an intersection of `c` elements of `g`. -/
-theorem mem_cardinaleGenerate_iff {s : Set α} {hreg : c.IsRegular} :
+theorem mem_cardinalGenerate_iff {s : Set α} {hreg : c.IsRegular} :
     s ∈ cardinalGenerate g (IsRegular.nat_lt hreg 2) ↔
     ∃ S : Set (Set α), S ⊆ g ∧ (#S < c) ∧ ⋂₀ S ⊆ s := by
   constructor <;> intro h
@@ -324,6 +325,8 @@ theorem mem_cardinaleGenerate_iff {s : Set α} {hreg : c.IsRegular} :
   exact mem_of_superset ((cardinal_sInter_mem Sct).mpr
     (fun s H => CardinalGenerateSets.basic (Sg H))) hS
 
+@[deprecated (since := "2025-11-14")] alias mem_cardinaleGenerate_iff := mem_cardinalGenerate_iff
+
 theorem le_cardinalGenerate_iff_of_cardinalInterFilter {f : Filter α} [CardinalInterFilter f c]
     (hc : 2 < c) : f ≤ cardinalGenerate g hc ↔ g ⊆ f.sets := by
   constructor <;> intro h
@@ -335,7 +338,7 @@ theorem le_cardinalGenerate_iff_of_cardinalInterFilter {f : Filter α} [Cardinal
   | superset _ st ih => exact mem_of_superset ih st
   | sInter Sct _ ih => exact (cardinal_sInter_mem Sct).mpr ih
 
-/-- `cardinalGenerate g hc` is the greatest `cardinalInterFilter c` containing `g`. -/
+/-- `cardinalGenerate g hc` is the greatest `CardinalInterFilter c` containing `g`. -/
 theorem cardinalGenerate_isGreatest (hc : 2 < c) :
     IsGreatest { f : Filter α | CardinalInterFilter f c ∧ g ⊆ f.sets } (cardinalGenerate g hc) := by
   refine ⟨⟨cardinalInter_ofCardinalGenerate _ _, fun s => CardinalGenerateSets.basic⟩, ?_⟩