diff --git a/Mathlib.lean b/Mathlib.lean
index bb572a5a061e4f..5c90675e2776af 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -7008,6 +7008,7 @@ public import Mathlib.SetTheory.Cardinal.Arithmetic
 public import Mathlib.SetTheory.Cardinal.Basic
 public import Mathlib.SetTheory.Cardinal.Cofinality.Basic
 public import Mathlib.SetTheory.Cardinal.Cofinality.Club
+public import Mathlib.SetTheory.Cardinal.Cofinality.Filter
 public import Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
 public import Mathlib.SetTheory.Cardinal.Continuum
 public import Mathlib.SetTheory.Cardinal.CountableCover
diff --git a/Mathlib/Algebra/Ring/BooleanRing.lean b/Mathlib/Algebra/Ring/BooleanRing.lean
index c71d7604fa6e0d..1f1973349f674a 100644
--- a/Mathlib/Algebra/Ring/BooleanRing.lean
+++ b/Mathlib/Algebra/Ring/BooleanRing.lean
@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Group.Idempotent
 public import Mathlib.Algebra.Ring.Equiv
 public import Mathlib.Algebra.Ring.PUnit
 public import Mathlib.Order.Hom.BoundedLattice
+public import Mathlib.RingTheory.Ideal.Quotient.Defs
 public import Mathlib.Tactic.Abel
 public import Mathlib.Tactic.Ring
 
@@ -105,6 +106,13 @@ instance (priority := 100) toCommRing : CommRing α :=
   { (inferInstance : BooleanRing α) with
     mul_comm := fun a b => by rw [← add_eq_zero', mul_add_mul] }
 
+instance (I : Ideal α) [I.IsTwoSided] : BooleanRing (α ⧸ I) where
+  isIdempotentElem x := by
+    apply Quotient.ind
+    intro x
+    change ⟦x * x⟧ = ⟦x⟧
+    rw [isIdempotentElem x]
+
 end BooleanRing
 
 instance : BooleanRing PUnit :=
@@ -149,6 +157,11 @@ theorem toBoolAlg_inj {a b : α} : toBoolAlg a = toBoolAlg b ↔ a = b :=
 theorem ofBoolAlg_inj {a b : AsBoolAlg α} : ofBoolAlg a = ofBoolAlg b ↔ a = b :=
   Iff.rfl
 
+/-- A recursor for `AsBoolAlg`. Use as `induction x`. -/
+@[elab_as_elim, induction_eliminator, cases_eliminator]
+protected def AsBoolAlg.rec {β : AsBoolAlg α → Sort*} (ind : ∀ a, β (toBoolAlg a)) :
+    ∀ a, β a := fun a ↦ ind (ofBoolAlg a)
+
 instance [Inhabited α] : Inhabited (AsBoolAlg α) :=
   ‹Inhabited α›
 
@@ -367,6 +380,11 @@ theorem toBoolRing_inj {a b : α} : toBoolRing a = toBoolRing b ↔ a = b :=
 theorem ofBoolRing_inj {a b : AsBoolRing α} : ofBoolRing a = ofBoolRing b ↔ a = b :=
   Iff.rfl
 
+/-- A recursor for `AsBoolRing`. Use as `induction x`. -/
+@[elab_as_elim, induction_eliminator, cases_eliminator]
+protected def AsBoolRing.rec {β : AsBoolRing α → Sort*} (ind : ∀ a, β (toBoolRing a)) :
+    ∀ a, β a := fun a ↦ ind (ofBoolRing a)
+
 instance [Inhabited α] : Inhabited (AsBoolRing α) :=
   ⟨default (α := α)⟩
 
@@ -471,6 +489,19 @@ theorem toBoolRing_inf (a b : α) : toBoolRing (a ⊓ b) = toBoolRing a * toBool
 theorem toBoolRing_symmDiff (a b : α) : toBoolRing (a ∆ b) = toBoolRing a + toBoolRing b :=
   rfl
 
+@[simp]
+theorem toBoolRing_compl (a : α) : toBoolRing aᶜ = 1 + toBoolRing a := by
+  rw [← top_symmDiff, toBoolRing_symmDiff, toBoolRing_top]
+
+@[simp]
+theorem toBoolRing_sup (a b : α) :
+    toBoolRing (a ⊔ b) = toBoolRing a + toBoolRing b + toBoolRing a * toBoolRing b := by
+  rw [← symmDiff_symmDiff_inf, toBoolRing_symmDiff, toBoolRing_symmDiff, toBoolRing_inf]
+
+@[simp]
+theorem toBoolRing_sdiff (a b : α) : toBoolRing (a \ b) = toBoolRing a * (1 + toBoolRing b) := by
+  simp [sdiff_eq]
+
 /-- Turn a bounded lattice homomorphism from Boolean algebras `α` to `β` into a ring homomorphism
 from `α` to `β` considered as Boolean rings. -/
 @[simps]
diff --git a/Mathlib/Order/Cofinal.lean b/Mathlib/Order/Cofinal.lean
index ce94954545c4d6..0eddfbd7bccbca 100644
--- a/Mathlib/Order/Cofinal.lean
+++ b/Mathlib/Order/Cofinal.lean
@@ -52,6 +52,11 @@ theorem IsCofinal.mono {s t : Set α} (h : s ⊆ t) (hs : IsCofinal s) : IsCofin
   obtain ⟨b, hb, hb'⟩ := hs a
   exact ⟨b, h hb, hb'⟩
 
+theorem IsCofinal.nonempty [Nonempty α] {s : Set α} (h : IsCofinal s) : s.Nonempty := by
+  inhabit α
+  obtain ⟨x, hx, _⟩ := h default
+  exact ⟨x, hx⟩
+
 end LE
 
 section Preorder
diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean
index 7aa88a68cc09b1..20ce62e446cb97 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean
@@ -12,9 +12,11 @@ public import Mathlib.SetTheory.Cardinal.Cofinality.Basic
 /-!
 # Club sets
 
-A subset of a well-ordered type `α` is called a club set when it is closed in the order topology and
-cofinal. If `α` has no maximum, then an equivalent condition is that `α` is closed and unbounded;
-hence the name.
+A subset of a well-ordered type `α` is called a **club set** when it is closed in the order topology
+and cofinal. If `α` has no maximum, then an equivalent condition is that `α` is closed and
+unbounded; hence the name.
+
+A **stationary set** is a set which intersects all club sets.
 
 ## Implementation notes
 
@@ -27,7 +29,9 @@ public section
 
 universe u v
 
-open Cardinal Order
+open Cardinal Order Set
+
+variable {α : Type v} {s t : Set α} {x : α} [LinearOrder α]
 
 /-- A club set is closed under suprema and cofinal. -/
 structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where
@@ -40,8 +44,6 @@ structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where
 
 namespace IsClub
 
-variable {α : Type v} {s t : Set α} {x : α} [LinearOrder α]
-
 @[simp]
 theorem of_isEmpty [IsEmpty α] {s : Set α} : IsClub s :=
   ⟨.of_isEmpty, .of_isEmpty⟩
@@ -50,6 +52,12 @@ theorem of_isEmpty [IsEmpty α] {s : Set α} : IsClub s :=
 protected theorem univ : IsClub (α := α) .univ :=
   ⟨.univ, .univ⟩
 
+protected theorem nonempty [Nonempty α] (hs : IsClub s) : s.Nonempty :=
+  hs.isCofinal.nonempty
+
+theorem _root_.isClub_empty_iff : IsClub (α := α) ∅ ↔ IsEmpty α :=
+  ⟨fun h ↦ isCofinal_empty_iff.1 h.isCofinal, fun _ ↦ .of_isEmpty⟩
+
 protected theorem union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) :=
   ⟨hs.dirSupClosed.union ht.dirSupClosed, hs.isCofinal.mono Set.subset_union_left⟩
 
@@ -63,12 +71,12 @@ theorem csSup_mem {α} [ConditionallyCompleteLinearOrder α] {s t : Set α}
 theorem sInter_of_orderTop {s : Set (Set α)} [OrderTop α] (hs : ∀ x ∈ s, IsClub x) :
     IsClub (⋂₀ s) := by
   refine ⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, ?_⟩
-  rw [isCofinal_iff_top_mem, Set.mem_sInter]
+  rw [isCofinal_iff_top_mem, mem_sInter]
   exact fun x hx ↦ (hs x hx).isCofinal.top_mem
 
 theorem iInter_of_orderTop {ι : Type*} {f : ι → Set α} [OrderTop α] (hs : ∀ i, IsClub (f i)) :
     IsClub (⋂ i, f i) := by
-  rw [← Set.sInter_range]
+  rw [← sInter_range]
   exact .sInter_of_orderTop (by simpa)
 
 theorem sInter_of_cof_le_one {s : Set (Set α)} (hα : cof α ≤ 1) (hs : ∀ x ∈ s, IsClub x) :
@@ -80,11 +88,10 @@ theorem sInter_of_cof_le_one {s : Set (Set α)} (hα : cof α ≤ 1) (hs : ∀ x
 
 theorem iInter_of_cof_le_one {ι : Type*} {f : ι → Set α} (hα : cof α ≤ 1) (hs : ∀ i, IsClub (f i)) :
     IsClub (⋂ i, f i) := by
-  rw [← Set.sInter_range]
+  rw [← sInter_range]
   exact .sInter_of_cof_le_one hα (by simpa)
 
 section WellFoundedLT
-
 variable [WellFoundedLT α]
 
 attribute [local instance]
@@ -102,7 +109,7 @@ protected theorem sInter {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : #s
     refine .of_not_isCofinal fun hg ↦ (cof_le hg).not_gt (hα.trans_le' ?_)
     simpa using mk_range_le_lift (f := g)
   refine ⟨_, fun t ht ↦ ?_, le_csSup hg ⟨0, rfl⟩⟩
-  apply (hs t ht).isLUB_mem (t := .range fun n ↦ f ⟨t, ht⟩ (g n)) _ (Set.range_nonempty _)
+  apply (hs t ht).isLUB_mem (t := .range fun n ↦ f ⟨t, ht⟩ (g n)) _ (range_nonempty _)
   · refine ⟨?_, fun b hb ↦ csSup_le' ?_⟩ <;> rintro _ ⟨n, rfl⟩
     · apply (le_csSup (.of_not_isCofinal _) _).trans (le_csSup hg ⟨n + 1, rfl⟩)
       · exact fun hg' ↦ (cof_le hg').not_gt (mk_range_le.trans_lt hsα)
@@ -113,28 +120,36 @@ protected theorem sInter {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : #s
 protected theorem iInter {ι : Type u} {f : ι → Set α} (hα : cof α ≠ ℵ₀)
     (hι : Cardinal.lift.{v} #ι < Cardinal.lift.{u} (cof α)) (hf : ∀ i, IsClub (f i)) :
     IsClub (⋂ i, f i) := by
-  rw [← Set.sInter_range]
+  rw [← sInter_range]
   refine IsClub.sInter hα ?_ (by simpa)
   rw [← Cardinal.lift_lt]
   exact mk_range_le_lift.trans_lt hι
 
-protected theorem inter {s t : Set α} (hα : cof α ≠ ℵ₀) (hs : IsClub s) (ht : IsClub t) :
-    IsClub (s ∩ t) := by
-  rw [← Set.sInter_pair]
-  have H : ∀ x ∈ ({s, t} : Set _), IsClub x := by simpa [hs]
-  obtain hα | hα' := hα.lt_or_gt
-  · rw [cof_lt_aleph0_iff] at hα
-    exact .sInter_of_cof_le_one hα H
-  · exact .sInter hα (hα'.trans_le' <| by simp) H
+theorem sInter_of_countable {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : s.Countable)
+    (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s) := by
+  obtain hα | hα := hα.lt_or_gt
+  · apply IsClub.sInter_of_cof_le_one _ hs
+    rwa [← cof_lt_aleph0_iff]
+  · apply IsClub.sInter hα.ne' (hα.trans_le' _) hs
+    rwa [le_aleph0_iff_set_countable]
+
+theorem iInter_of_countable {ι : Type*} {f : ι → Set α} [Countable ι] (hα : cof α ≠ ℵ₀)
+    (hf : ∀ i, IsClub (f i)) : IsClub (⋂ i, f i) := by
+  rw [← sInter_range]
+  apply IsClub.sInter_of_countable hα (countable_range f)
+  simpa
 
-theorem _root_.Order.IsNormal.isClub_range {f : α → α} (hf : IsNormal f) : IsClub (.range f) :=
+protected theorem inter (hα : cof α ≠ ℵ₀) (hs : IsClub s) (ht : IsClub t) : IsClub (s ∩ t) := by
+  simpa [hs, ht] using IsClub.sInter_of_countable (s := {s, t}) hα
+
+theorem Order.IsNormal.isClub_range {f : α → α} (hf : IsNormal f) : IsClub (.range f) :=
   ⟨hf.dirSupClosed_range, fun x ↦ ⟨_, ⟨x, rfl⟩, hf.strictMono.le_apply⟩⟩
 
 theorem _root_.Order.IsNormal.isClub_fixedPoints {f : α → α} (hα : cof α ≠ ℵ₀) (hf : IsNormal f) :
     IsClub f.fixedPoints := by
   cases isEmpty_or_nonempty α; · simp
   refine ⟨fun s hs hs₀ _ a ha ↦ (hf.map_isLUB ha hs₀).unique ?_, fun a ↦ ?_⟩
-  · rwa [Set.image_congr hs, Set.image_id']
+  · rwa [image_congr hs, image_id']
   · cases topOrderOrNoTopOrder α with
     | inl => use ⊤; simpa using hf.strictMono.id_le ⊤
     | inr h =>
@@ -147,3 +162,115 @@ theorem _root_.Order.IsNormal.isClub_fixedPoints {f : α → α} (hα : cof α 
 
 end WellFoundedLT
 end IsClub
+
+/-! ### Stationary sets -/
+
+/-- A set is called stationary when it intersects all club sets. -/
+@[expose]
+def IsStationary (s : Set α) : Prop :=
+  ∀ ⦃t⦄, IsClub t → (s ∩ t).Nonempty
+
+theorem not_isStationary_iff : ¬ IsStationary s ↔ ∃ t, IsClub t ∧ Disjoint s t := by
+  simp [IsStationary, disjoint_iff, not_nonempty_iff_eq_empty]
+
+@[gcongr]
+theorem IsStationary.mono (hs : IsStationary s) (h : s ⊆ t) : IsStationary t :=
+  fun _u hu ↦ (hs hu).mono (inter_subset_inter_left _ h)
+
+theorem IsStationary.nonempty (hs : IsStationary s) : s.Nonempty := by
+  simpa using hs .univ
+
+theorem isStationary_univ_iff : IsStationary (.univ (α := α)) ↔ Nonempty α := by
+  simp [IsStationary, ← not_imp_not (b := IsClub _), not_nonempty_iff_eq_empty,
+    isClub_empty_iff]
+
+@[simp]
+protected theorem IsStationary.univ [Nonempty α] : IsStationary (.univ (α := α)) :=
+  isStationary_univ_iff.2 ‹_›
+
+@[simp]
+theorem not_isStationary_empty : ¬ IsStationary (∅ : Set α) := by
+  intro h
+  simpa using h .univ
+
+@[simp]
+theorem not_isStationary_of_isEmpty [IsEmpty α] : ¬ IsStationary s :=
+  s.eq_empty_of_isEmpty ▸ not_isStationary_empty
+
+theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal sᶜ) : IsStationary s := by
+  intro t ht
+  obtain ⟨a, ha⟩ := not_isCofinal_iff.1 hs
+  obtain ⟨b, hb, hb'⟩ := ht.isCofinal a
+  refine ⟨b, ?_, hb⟩
+  contrapose! ha
+  exact ⟨b, ha, hb'⟩
+
+theorem isStationary_sUnion_iff_of_cof_le_one {s : Set (Set α)} (hα : cof α ≤ 1) :
+    IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x where
+  mp h := by
+    contrapose! h
+    simp_rw [not_isStationary_iff] at h ⊢
+    choose f hf hxf using h
+    refine ⟨⋂ x : s, f _ x.2, ?_, ?_⟩
+    · apply IsClub.iInter_of_cof_le_one hα
+      simpa
+    · rw [disjoint_sUnion_left]
+      exact fun x hx ↦ (hxf _ hx).mono_right (iInter_subset _ ⟨x, hx⟩)
+  mpr := fun ⟨x, hxs, hx⟩ ↦ hx.mono (subset_sUnion_of_mem hxs)
+
+theorem isStationary_iUnion_iff_of_cof_le_one {ι : Type u} {f : ι → Set α} (hα : cof α ≤ 1) :
+    IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i) := by
+  rw [← sUnion_range, isStationary_sUnion_iff_of_cof_le_one hα]
+  simp
+
+theorem isStationary_sUnion_iff_of_orderTop [OrderTop α] {s : Set (Set α)} :
+    IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x :=
+  isStationary_sUnion_iff_of_cof_le_one (by simp)
+
+theorem isStationary_iUnion_iff_of_orderTop [OrderTop α] {ι : Type u} {f : ι → Set α} :
+    IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i) :=
+  isStationary_iUnion_iff_of_cof_le_one (by simp)
+
+section WellFoundedLT
+variable [WellFoundedLT α]
+
+theorem IsClub.isStationary [Nonempty α] (hα : cof α ≠ ℵ₀) (hs : IsClub s) : IsStationary s :=
+  fun _ ht ↦ (hs.inter hα ht).nonempty
+
+theorem isStationary_sUnion_iff {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : #s < cof α) :
+    IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x where
+  mp h := by
+    contrapose! h
+    simp_rw [not_isStationary_iff] at h ⊢
+    choose f hf hxf using h
+    refine ⟨⋂ x : s, f _ x.2, ?_, ?_⟩
+    · apply IsClub.iInter hα <;> simpa
+    · rw [disjoint_sUnion_left]
+      exact fun x hx ↦ (hxf _ hx).mono_right (iInter_subset _ ⟨x, hx⟩)
+  mpr := fun ⟨x, hxs, hx⟩ ↦ hx.mono (subset_sUnion_of_mem hxs)
+
+theorem isStationary_iUnion_iff {ι : Type u} {f : ι → Set α} (hα : cof α ≠ ℵ₀)
+    (hι : lift.{v} #ι < lift.{u} (cof α)) : IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i) := by
+  rw [← sUnion_range, isStationary_sUnion_iff hα]
+  · simp
+  · rw [← Cardinal.lift_lt]
+    exact mk_range_le_lift.trans_lt hι
+
+theorem isStationary_sUnion_iff_of_countable {s : Set (Set α)} (hα : cof α ≠ ℵ₀)
+    (hsα : s.Countable) : IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x := by
+  obtain hα | hα := hα.lt_or_gt
+  · apply isStationary_sUnion_iff_of_cof_le_one
+    rwa [← cof_lt_aleph0_iff]
+  · apply isStationary_sUnion_iff hα.ne' (hα.trans_le' _)
+    rwa [le_aleph0_iff_set_countable]
+
+theorem isStationary_iUnion_iff_of_countable {ι : Type*} {f : ι → Set α} [Countable ι]
+    (hα : cof α ≠ ℵ₀) : IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i) := by
+  rw [← sUnion_range, isStationary_sUnion_iff_of_countable hα (countable_range f)]
+  simp
+
+theorem isStationary_union_iff (hα : cof α ≠ ℵ₀) :
+    IsStationary (s ∪ t) ↔ IsStationary s ∨ IsStationary t := by
+  simpa using isStationary_sUnion_iff_of_countable (s := {s, t}) hα
+
+end WellFoundedLT
diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Filter.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Filter.lean
new file mode 100644
index 00000000000000..284a0719f0dbdf
--- /dev/null
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Filter.lean
@@ -0,0 +1,158 @@
+/-
+Copyright (c) 2026 Violeta Hernández Palacios. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Violeta Hernández Palacios
+-/
+module
+
+public import Mathlib.Algebra.Ring.BooleanRing
+public import Mathlib.Order.Filter.CardinalInter
+public import Mathlib.RingTheory.Ideal.Quotient.Defs
+public import Mathlib.SetTheory.Cardinal.Cofinality.Club
+
+/-!
+# The club filter and the non-stationary ideal
+
+Let `α` be a well-order of uncountable cofinality. We are interested in two constructions:
+
+- The `clubFilter` is a filter on `α`, consisting of all sets which contain a club. It is closed
+  under intersections of cardinal `cof α`.
+- The `nonstationaryIdeal` is an ideal on `α`, consisting of non-stationary sets. It is closed under
+  unions of cardinal `cof α`.
+
+
+
+## Implementation details
+
+It'd be most natural to define `nonstationaryIdeal` using `Order.Ideal`, but Mathlib currently has
+no way of taking a quotient by it. We instead define it as a (ring) `Ideal` on the type alias
+`AsBoolRing (Set α)`. This lets us define `StationarySet` as a ring quotient.
+-/
+
+#exit
+@[expose] public section
+
+variable {α : Type*} {s : Set α} [LinearOrder α] [WellFoundedLT α]
+
+open Cardinal Order Set
+
+/-! ### Filter and ideal -/
+
+/-- The filter consisting of all sets which contain a club set. -/
+@[simps]
+def clubFilter (hα : cof α ≠ ℵ₀) : Filter α where
+  sets := {s | ∃ t ⊆ s, IsClub t}
+  univ_sets := ⟨_, subset_rfl, .univ⟩
+  sets_of_superset {s t} hs hst := by
+    obtain ⟨u, hus, hu⟩ := hs
+    exact ⟨u, hus.trans hst, hu⟩
+  inter_sets {s t} hs ht := by
+    obtain ⟨u, hus, hu⟩ := hs
+    obtain ⟨v, hvt, hv⟩ := ht
+    exact ⟨_, Set.inter_subset_inter hus hvt, hu.inter hα hv⟩
+
+@[simp]
+theorem mem_clubFilter {hα : cof α ≠ ℵ₀} : s ∈ clubFilter hα ↔ ∃ t ⊆ s, IsClub t :=
+  .rfl
+
+theorem cardinalInterFilter_clubFilter {hα : cof α ≠ ℵ₀} :
+    CardinalInterFilter (clubFilter hα) (cof α) where
+  cardinal_sInter_mem s hsα hs := by
+    simp_rw [mem_clubFilter] at hs
+    choose t hts ht using hs
+    refine ⟨⋂ x : s, t _ x.2, ?_, ?_⟩
+    · rw [Set.sInter_eq_iInter]
+      exact Set.iInter_mono (by simpa)
+    · apply IsClub.iInter hα <;> simpa
+
+theorem countableInterFilter_clubFilter {hα : cof α ≠ ℵ₀} :
+    CountableInterFilter (clubFilter hα) where
+  countable_sInter_mem s hsα hs := by
+    simp_rw [mem_clubFilter] at hs
+    choose t hts ht using hs
+    refine ⟨⋂ x : s, t _ x.2, ?_, ?_⟩
+    · rw [Set.sInter_eq_iInter]
+      exact Set.iInter_mono (by simpa)
+    · have := hsα.to_subtype
+      apply IsClub.iInter_of_countable hα
+      simpa
+
+@[simps]
+def nonstationaryIdeal (hα : cof α ≠ ℵ₀) : Ideal (AsBoolRing (Set α)) where
+  carrier := {s | ¬ IsStationary (ofBoolRing s)}
+  zero_mem' := by simp
+  add_mem' {s t} hs ht := by
+    dsimp at *
+    rw [Set.symmDiff_def, isStationary_union_iff hα, not_or]
+    constructor
+    · contrapose! hs
+      exact hs.mono diff_subset
+    · contrapose! ht
+      exact ht.mono diff_subset
+  smul_mem' s t hs := by
+    dsimp at *
+    contrapose! hs
+    exact hs.mono inter_subset_right
+
+@[simp]
+theorem mem_nonstationaryIdeal_iff {s : AsBoolRing (Set α)} {hα : cof α ≠ ℵ₀} :
+    s ∈ nonstationaryIdeal hα ↔ ¬ IsStationary (ofBoolRing s) :=
+  .rfl
+
+/-! ### Boolean algebra of stationary sets -/
+
+variable [h₀ : Fact (cof α ≠ ℵ₀)]
+include h₀
+
+variable (α) in
+def StationarySet : Type _ :=
+  AsBoolRing (Set α) ⧸ nonstationaryIdeal h₀.out
+
+namespace StationarySet
+
+instance : BooleanAlgebra (StationarySet α) :=
+  let : BooleanRing (StationarySet α) :=
+    inferInstanceAs (BooleanRing (AsBoolRing (Set α) ⧸ nonstationaryIdeal h₀.out))
+  BooleanRing.toBooleanAlgebra
+
+def mk (s : Set α) : StationarySet α :=
+  Ideal.Quotient.mk _ (toBoolRing s)
+
+theorem mk_eq_mk {s t : Set α} : mk s = mk t ↔ ¬ IsStationary (symmDiff s t) :=
+  Ideal.Quotient.mk_eq_mk_iff_sub_mem ..
+
+@[simp] theorem mk_empty : mk (∅ : Set α) = ⊥ := rfl
+@[simp] theorem mk_univ : mk (univ : Set α) = ⊤ := rfl
+@[simp] theorem mk_inter (s t : Set α) : mk (s ∩ t) = mk s ⊓ mk t := rfl
+
+@[simp]
+theorem mk_compl (s : Set α) : mk sᶜ = (mk s)ᶜ := by
+  unfold mk
+  rw [toBoolRing_compl]
+  rfl
+
+@[simp]
+theorem mk_union (s t : Set α) : mk (s ∪ t) = mk s ⊔ mk t := by
+  change mk (s ⊔ t) = _
+  unfold mk
+  rw [toBoolRing_sup]
+  rfl
+
+@[simp]
+theorem mk_sdiff (s t : Set α) : mk (s \ t) = mk s \ mk t := by
+  unfold mk
+  rw [toBoolRing_sdiff]
+  rfl
+
+@[simp]
+theorem mk_symmDiff (s t : Set α) : mk (symmDiff s t) = symmDiff (mk s) (mk t) := by
+  simp [symmDiff]
+
+@[simp]
+theorem mk_eq_bot {s : Set α} : mk s = ⊥ ↔ ¬ IsStationary s := by
+  rw [← mk_empty, mk_eq_mk]
+  simp [symmDiff]
+
+alias ⟨_, mk_of_not_isStationary⟩ := mk_eq_bot
+
+end StationarySet