diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index d84700594ff1ab..6361755ad71256 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -1,23 +1,26 @@
 /-
 Copyright (c) 2025 Peter Pfaffelhuber. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Rémy Degenne, Peter Pfaffelhuber
+Authors: Rémy Degenne, Peter Pfaffelhuber, Joachim Breitner
 -/
 import Mathlib.Data.Set.Dissipate
 import Mathlib.Logic.IsEmpty
 import Mathlib.MeasureTheory.Constructions.Cylinders
 import Mathlib.Order.OmegaCompletePartialOrder
 import Mathlib.Topology.Separation.Hausdorff
+
 /-!
 # Compact systems.
 
-This file defines compact systems of sets.
+This file defines compact systems of sets. These are set systems `p : Set α → Prop` with the
+following property: If `C : ℕ → Set α` is such that `∀ n, p (C n)` and `⋂ n, C n = ∅`, then
+there is some `N : ℕ` with `⋂ n < N, C n = ∅`.
 
 ## Main definitions
 
 * `IsCompactSystem`: A set of sets is a compact system if, whenever a countable subfamily has empty
   intersection, then finitely many of them already have empty intersection.
-
+* `IsCompactSystem.union`: The set system of finite unions of another set system.
 ## Main results
 
 * `IsCompactSystemiff_isCompactSystem_of_or_univ`: A set system is a compact
@@ -25,8 +28,10 @@ system iff inserting `univ` gives a compact system.
 * `IsClosedCompact.isCompactSystem`: The set of closed and compact sets is a compact system.
 * `IsClosedCompact.isCompactSystem_of_T2Space`: In a `T2Space α`, the set of compact sets
   is a compact system in a `T2Space`.
+* `IsCompactSystem.union.isCompactSystem`: If `IsCompactSystem p`, the set of finite unions
+  of `K : Set α` with `p K` is a compact system.
 * `IsCompactSystem.closedCompactSquareCylinders`: Closed and compact square cylinders form a
-  compact system.
+  compact system in a product space.
 -/
 
 open Set Nat MeasureTheory
@@ -86,6 +91,16 @@ lemma iff_nonempty_iInter_of_lt (p : Set α → Prop) : IsCompactSystem p ↔
     rw [mem_iInter₂, mem_iInter₂]
     exact fun h i hi ↦ h i hi.le
 
+lemma k (s : ℕ → Set α) (n : ℕ) : ⋂ (j < n), s j = ⋂ (j : Fin n), s j := by
+  ext x
+  simp only [mem_iInter]
+  refine ⟨fun h i ↦ h i.val i.prop, fun h i hi ↦ h ⟨i, hi⟩⟩
+
+lemma iff_nonempty_iInter_of_lt' (p : Set α → Prop) : IsCompactSystem p ↔
+    ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, (⋂ k : Fin n, C k).Nonempty) → (⋂ i, C i).Nonempty := by
+  rw [iff_nonempty_iInter_of_lt]
+  simp_rw [← k]
+
 /-- Any subset of a compact system is a compact system. -/
 theorem mono {C D : (Set α) → Prop} (hD : IsCompactSystem D) (hCD : ∀ s, C s → D s) :
   IsCompactSystem C := fun s hC hs ↦ hD s (fun i ↦ hCD (s i) (hC i)) hs
@@ -286,6 +301,293 @@ theorem of_isCompact [T2Space α] :
 
 end IsCompactIsClosed
 
+end IsCompactSystem
+
+section PrefixInduction
+
+/-- A version of `Fin.elim` using even more dependent types. -/
+def Fin.elim0'.{u} {α : ℕ → Sort u} : (i : Fin 0) → (α i)
+  | ⟨_, h⟩ => absurd h (Nat.not_lt_zero _)
+
+variable {β : ℕ → Type*}
+variable (q : ∀ n, (k : (i : Fin n) → (β i)) → Prop)
+variable (step0 : q 0 Fin.elim0')
+variable (step :
+    ∀ n (k : (i : Fin n) → (β i)) (_ : q n k),
+    { a : β n // q (n+1) (Fin.snoc k a)})
+
+/-- In this section, we prove a general induction principle, which we need for the construction
+`Nat.prefixInduction q step0 step : (k : ℕ) →  (β k)` based on some
+`q : (n : ℕ) → (k : (i : Fin n) → (β i)) → Prop`. For
+the inducation start, `step0 : q 0 _` always holds since `Fin 0` cannot be satisfied, and
+`step : (n : ℕ) → (k : (i : Fin n) → β i) → q n k → { a : β n // q (n + 1) (Fin.snoc k a) })`
+`(n : ℕ) : β n` constructs the next element satisfying `q (n + 1) _` from a proof of `q n k`
+and finding the next element.
+
+In comparisong to other induction principles, the proofs of `q n k` are needed in order to find
+the next element. -/
+
+/- An auxiliary definition for `Nat.prefixInduction`. -/
+def Nat.prefixInduction.aux : ∀ (n : Nat), { k : (i : Fin n) → (β i) // q n k }
+    | 0 => ⟨Fin.elim0', step0⟩
+    | n+1 =>
+      let ⟨k, hk⟩ := aux n
+      let ⟨a, ha⟩ := step n k hk
+      ⟨Fin.snoc k a, ha⟩
+
+theorem Nat.prefixInduction.auxConsistent :
+  ∀ n (i : Fin n),
+    (Nat.prefixInduction.aux q step0 step (i+1)).1 (Fin.last i) =
+    (Nat.prefixInduction.aux q step0 step n).1 i := by
+  intro n
+  induction n
+  next => simp
+  next n ih =>
+    apply Fin.lastCases
+    case last => simp
+    case cast =>
+      intro i
+      simp only [Fin.coe_castSucc]
+      rw [ih, aux]
+      simp
+
+/-- An induction principle showing that `q : (n : ℕ) → (k : (i : Fin n) → (β i)) → Prop` holds
+for all `n`. `step0` is satisfied by construction since `Fin 0` is empty.
+In the induction `step`, we use that `q n k` holds for showing that `q (n + 1) (Fin.snoc k a)`
+holds for some `a : β n`. -/
+def Nat.prefixInduction (n : Nat) : β n :=
+  (Nat.prefixInduction.aux q step0 step (n+1)).1 (Fin.last n)
+
+theorem Nat.prefixInduction_spec (n : Nat) : q n (Nat.prefixInduction q step0 step ·) := by
+  cases n
+  · convert step0
+  · next n =>
+    have hk := (Nat.prefixInduction.aux q step0 step (n+1)).2
+    convert hk with i
+    apply Nat.prefixInduction.auxConsistent
+
+/- Often, `step` can only be proved by showing an `∃` statement. For this case, we use `step'`. -/
+variable (step' : ∀ n (k : (i : Fin n) → (β i)) (_ : q n k), ∃ a, q (n + 1) (Fin.snoc k a))
+
+/-- For `Nat.prefixIndution`, this transforms an exists-statement in the induction step to choosing
+an element. -/
+noncomputable def step_of : (n : ℕ) → (k : (i : Fin n) → (β i)) → (hn : q n k) →
+    { a : β n // q (n + 1) (Fin.snoc k a) } :=
+  fun n k hn ↦ ⟨(step' n k hn).choose, (step' n k hn).choose_spec⟩
+
+/-- An induction principle showing that `q : (n : ℕ) → (k : (i : Fin n) → (β i)) → Prop` holds
+for all `n`. `step0` is satisfied by construction since `Fin 0` is empty.
+In the induction `step`, we use that `q n k` holds for showing that `q (n + 1) (Fin.snoc k a)`
+holds for some `a : β n`. This version is noncomputable since it relies on an `∃`-statement -/
+noncomputable def Nat.prefixInduction' (n : Nat) : β n :=
+  (Nat.prefixInduction.aux q step0 (fun n k hn ↦ step_of q step' n k hn) (n+1)).1 (Fin.last n)
+
+theorem Nat.prefixInduction'_spec (n : Nat) : q n (Nat.prefixInduction' q step0 step' ·) := by
+  apply prefixInduction_spec
+
+end PrefixInduction
+
+namespace IsCompactSystem
+
+section Union
+
+/-- `q n K` is the joint property that `∀ (k : Fin n), K k ∈ L k` and
+`∀ N, (⋂ (j : Fin n), K j) ∩ (⋂ (k < N), ⋃₀ (L (n + k)).toSet) ≠ ∅`.` holds. -/
+def q (L : ℕ → Finset (Set α))
+  : ∀ n, (K : (k : Fin n) → (L k)) → Prop := fun n K ↦
+  (∀ N, ((⋂ j, K j) ∩ (⋂ (k < N), ⋃₀ (L (n + k)).toSet)).Nonempty)
+
+lemma q_iff_iInter (L : ℕ → Finset (Set α)) (n : ℕ) (K : (k : Fin n) → (L k)) :
+    q L n K ↔ (∀ (N : ℕ), ((⋂ (j : ℕ) (hj : j < n), K ⟨j, hj⟩) ∩ (⋂ (k < N),
+    ⋃₀ (L (n + k)).toSet)).Nonempty) := by
+  simp [q]
+  refine ⟨fun h N ↦ ?_, fun h N ↦ ?_⟩ <;>
+  specialize h N <;>
+  rw [Set.inter_nonempty_iff_exists_left] at h ⊢ <;>
+  obtain ⟨x, ⟨hx1, hx2⟩⟩ := h <;>
+  refine ⟨x, ⟨?_, hx2⟩⟩ <;>
+  simp only [mem_iInter] at hx1 ⊢
+  · exact fun i hi ↦ hx1 ⟨i, hi⟩
+  · exact fun i ↦ hx1 i.val i.prop
+
+example (i : ℕ) (hi : i ≠ 0) : ∃ j, j + 1 = i := by
+  exact exists_add_one_eq.mpr (zero_lt_of_ne_zero hi)
+
+lemma q_iff_iInter' (L : ℕ → Finset (Set α)) (n : ℕ) (K : (k : Fin n) → (L k)) (y : L n) :
+    q L (n + 1) (Fin.snoc K y) ↔ (∀ (N : ℕ), ((⋂ (j : ℕ) (hj : j < n), K ⟨j, hj⟩) ∩ y.val ∩
+    (⋂ (k < N), ⋃₀ (L (n + k)).toSet)).Nonempty) := by
+  simp [q]
+  refine ⟨fun h N ↦ ?_, fun h N ↦ ?_⟩
+  · specialize h N
+    rw [Set.inter_nonempty_iff_exists_left] at h ⊢
+    obtain ⟨x, ⟨hx1, hx2⟩⟩ := h
+    use x
+    simp at hx1 hx2 ⊢
+    refine ⟨⟨?_, ?_⟩, ?_⟩
+    · intro i hi
+      specialize hx1 ⟨i, le_trans hi (le_succ n)⟩
+      simp [Fin.snoc, hi] at hx1
+      exact hx1
+    · specialize hx1 ⟨n, Nat.lt_add_one n⟩
+      simp [Fin.snoc] at hx1
+      exact hx1
+    · intro i hi
+      by_cases h : i = 0
+      · specialize hx1 ⟨n, Nat.lt_add_one n⟩
+        simp [Fin.snoc] at hx1
+        simp [h]
+        refine ⟨y, y.prop, hx1⟩
+      · obtain ⟨j, hj⟩ := exists_add_one_eq.mpr (zero_lt_of_ne_zero h)
+        have hj' : j < N := by
+          rw [← hj] at hi
+          exact lt_of_succ_lt hi
+        specialize hx2 j hj'
+        rw [add_comm] at hj
+        rw [add_assoc, hj] at hx2
+        exact hx2
+  · specialize h (N + 1)
+    rw [Set.inter_nonempty_iff_exists_left] at h ⊢
+    obtain ⟨x, ⟨hx1, hx2⟩⟩ := h
+    use x
+    simp at hx1 hx2 ⊢
+    refine ⟨?_, ?_⟩
+    · intro i
+      simp [Fin.snoc]
+      refine Fin.lastCases ?_ (fun i ↦ ?_) i
+      · simp [Fin.snoc_last]
+        exact hx1.2
+      · simp [Fin.snoc_castSucc]
+        exact hx1.1 i.val i.prop
+    · intro i hi
+      specialize hx2 (i + 1) (Nat.add_lt_add_right hi 1)
+      rw [add_assoc, add_comm 1 i]
+      exact hx2
+
+lemma step0 {L : ℕ → Finset (Set α)} (hL : ∀ N, (⋂ k, ⋂ (_ : k < N), ⋃₀ (L k).toSet).Nonempty) :
+    q L 0 (Fin.elim0' (α := fun n ↦ {a : Set α // a ∈ L n})) := by
+  intro N
+  simp only [iInter_of_empty, zero_add, univ_inter]
+  exact hL N
+
+lemma inter_sUnion_eq_empty (s : Set α) (L : Set (Set α)) :
+    (∀ a ∈ L, s ∩ a = ∅) ↔ s ∩ ⋃₀ L = ∅ := by
+  simp_rw [← disjoint_iff_inter_eq_empty]
+  rw [disjoint_sUnion_right]
+
+lemma step' {L : ℕ → Finset (Set α)}
+    : ∀ n (K : (k : Fin n) → L k), (q L n K) → ∃ a, q L (n + 1) (Fin.snoc K a) := by
+  intro n K hK
+  simp_rw [q_iff_iInter] at hK
+  simp_rw [q_iff_iInter'] at ⊢
+  by_contra! h
+  choose b hb using h
+  classical
+  let b' := fun x ↦ dite (x ∈ (L n)) (fun c ↦ b ⟨x, c⟩) (fun _ ↦ 0)
+  have hs : (L n).toSet.Nonempty := by
+    specialize hK 1
+    rw [nonempty_def] at hK ⊢
+    simp only [lt_one_iff, iInter_iInter_eq_left, add_zero, mem_inter_iff, mem_iInter, mem_sUnion,
+      Finset.mem_coe] at hK ⊢
+    obtain ⟨x, ⟨hx1, ⟨t, ⟨ht1, ht2⟩⟩⟩⟩ := hK
+    use t
+  obtain ⟨K0Max, ⟨hK0₁, hK0₂⟩⟩ := Finset.exists_max_image (L (Fin.last n)) b' hs
+  simp_rw [nonempty_iff_ne_empty] at hK
+  apply hK (b' K0Max + 1)
+  have h₂ (a : L n) : ⋂ k < b' K0Max, ⋃₀ (L (n + k)) ⊆ ⋂ k, ⋂ (_ : k < b a),
+      ⋃₀ (L (n + k)).toSet := by
+    intro x hx
+    simp at hx ⊢
+    have f : b' a = b a := by
+      simp [b']
+    exact fun i hi ↦ hx i (lt_of_lt_of_le hi (f ▸ hK0₂ a.val a.prop))
+  have h₃ : ∀ (a : { x // x ∈ L ↑(Fin.last n) }), (⋂ j, ⋂ (hj : j < n), ↑(K ⟨j, hj⟩)) ∩ ↑a ∩
+      ⋂ k, ⋂ (_ : k < b' K0Max), ⋃₀ (L (n + k)).toSet = ∅ := by
+    intro a
+    rw [← subset_empty_iff, ← hb a]
+    apply inter_subset_inter (fun ⦃a⦄ a ↦ a) (h₂ a)
+  simp_rw [inter_comm, inter_assoc] at h₃
+  simp_rw [← disjoint_iff_inter_eq_empty] at h₃ ⊢
+  simp at h₃
+  have h₃' := disjoint_sUnion_left.mpr h₃
+  rw [disjoint_iff_inter_eq_empty, inter_comm, inter_assoc, ← disjoint_iff_inter_eq_empty] at h₃'
+  apply disjoint_of_subset (fun ⦃a⦄ a ↦ a) _ h₃'
+  simp only [subset_inter_iff, subset_iInter_iff]
+  refine ⟨fun i hi x hx ↦ ?_, fun x hx ↦ ?_⟩
+  · simp at hx ⊢
+    obtain ⟨t, ht⟩ := hx i (lt_trans hi (Nat.lt_add_one _))
+    use t
+  · simp at hx ⊢
+    obtain ⟨t, ht⟩ := hx 0 (zero_lt_succ _)
+    simp at ht
+    use t
+    exact ht
+
+/-- For `L : ℕ → Finset (Set α)` such that `∀ K ∈ L n, p K` and
+`h : ∀ N, ⋂ k < N, ⋃₀ L k ≠ ∅`, `mem_of_union h n` is some `K : ℕ → Set α` such that `K n ∈ L n`
+for all `n` (this is `prop₀`) and `∀ N, ⋂ (j < n, K j) ∩ ⋂ (k < N), (⋃₀ L (n + k)) ≠ ∅`
+(this is `prop₁`.) -/
+noncomputable def mem_of_union (L : ℕ → Finset (Set α))
+  (hL : ∀ N, (⋂ k, ⋂ (_ : k < N), ⋃₀ (L k).toSet).Nonempty) : (k : ℕ) → L k :=
+  Nat.prefixInduction' (q L) (step0 hL) (step')
+
+theorem mem_of_union.spec (L : ℕ → Finset (Set α))
+    (hL : ∀ N, (⋂ k, ⋂ (_ : k < N), ⋃₀ (L k).toSet).Nonempty) (n : ℕ) :
+    (∀ N, ((⋂ (j : Fin n), (mem_of_union L hL) j) ∩ (⋂ (k < N), ⋃₀ (L (n + k)).toSet)).Nonempty) :=
+  Nat.prefixInduction'_spec (β := fun n ↦ {a // a ∈ L n}) (q L) (step0 hL) (step') n
+
+lemma l1 (L : ℕ → Finset (Set α))
+    (hL : ∀ N, (⋂ k, ⋂ (_ : k < N), ⋃₀ (L k).toSet).Nonempty) (k : ℕ) :
+      (mem_of_union L hL k).val ∈ (L k).toSet := by
+  exact (mem_of_union L hL k).prop
+
+lemma sInter_memOfUnion_nonempty (L : ℕ → Finset (Set α))
+    (hL : ∀ N, (⋂ k, ⋂ (_ : k < N), ⋃₀ (L k).toSet).Nonempty) (n : ℕ) :
+    (⋂ (j : Fin n), (mem_of_union L hL j).val).Nonempty := by
+  have h := mem_of_union.spec L hL n 0
+  simp only [not_lt_zero, iInter_of_empty, iInter_univ, inter_univ] at h
+  exact h
+
+lemma sInter_memOfUnion_isSubset (L : ℕ → Finset (Set α))
+    (hL : ∀ N, (⋂ k < N, ⋃₀ (L k).toSet).Nonempty) :
+    (⋂ j, (mem_of_union L hL j)) ⊆ ⋂ k, (⋃₀ (L k).toSet) := by
+  exact iInter_mono <| fun n ↦
+  subset_sUnion_of_subset (↑(L n)) (mem_of_union L hL n).val (fun ⦃a⦄ a ↦ a) (l1 L hL n)
+
+/-- Finite unions of sets in a compact system. -/
+def union (p : Set α → Prop) : Set α → Prop :=
+  (sUnion '' ({ L : Set (Set α) | L.Finite ∧ ∀ K ∈ L, p K}))
+
+lemma union.mem_iff (s : Set α) : union p s ↔ ∃ L : Finset (Set α), s = ⋃₀ L ∧ ∀ K ∈ L, p K := by
+  refine ⟨fun ⟨L, hL⟩ ↦ ?_, fun h ↦ ?_⟩
+  · simp only [mem_setOf_eq] at hL
+    let L' := (hL.1.1).toFinset
+    use L'
+    rw [← hL.2, Finite.coe_toFinset]
+    refine ⟨rfl, fun K hK ↦ ?_⟩
+    rw [Finite.mem_toFinset] at hK
+    apply hL.1.2 K hK
+  · obtain ⟨L, hL⟩ := h
+    use L
+    simp only [mem_setOf_eq, Finset.finite_toSet, Finset.mem_coe, true_and]
+    refine ⟨hL.2, hL.1.symm⟩
+
+theorem union.isCompactSystem (p : Set α → Prop)(hp : IsCompactSystem p) :
+    IsCompactSystem (union p) := by
+  rw [iff_nonempty_iInter_of_lt]
+  intro C hi
+  simp_rw [mem_iff] at hi
+  choose L' hL' using hi
+  simp_rw [hL']
+  intro hL
+  have h₁ := sInter_memOfUnion_nonempty L' hL
+  have h₂ : (∀ (i : ℕ), p ↑(mem_of_union L' hL i)) :=
+    fun i ↦ (hL' i).2 (mem_of_union L' hL i).val (mem_of_union L' hL i).prop
+  have h₃ := (iff_nonempty_iInter_of_lt' p).mp hp (fun k ↦ (mem_of_union L' hL k).val) h₂ h₁
+  have h₄ : ⋂ i, (mem_of_union L' hL) i ⊆ ⋂ i, ⋃₀ (L' i).toSet := sInter_memOfUnion_isSubset L' hL
+  exact Nonempty.mono h₄ h₃
+
+end Union
+
 section pi
 
 variable {ι : Type*}  {α : ι → Type*}
@@ -367,7 +669,7 @@ closed and compact, for all `i ∈ s`. -/
 def MeasureTheory.compactClosedSquareCylinders : Set (Set (Π i, α i)) :=
   MeasureTheory.squareCylinders (fun i ↦ { t : Set (α i) | IsCompact t ∧ IsClosed t })
 
-/-- Products of compact and closed sets form a a compact system. -/
+/-- Products of compact and closed sets form a compact system. -/
 theorem IsCompactSystem.compactClosedPi :
     IsCompactSystem (univ.pi '' univ.pi (fun i ↦ { t : Set (α i) | IsCompact t ∧ IsClosed t })) :=
   IsCompactSystem.pi _ (fun _ ↦ IsCompactSystem.of_isCompact_isClosed)