From ac22b1b7f937461b56b6989f3ab40c6a50bc3c74 Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Wed, 12 Feb 2025 18:20:39 +0100
Subject: [PATCH 01/53] started compactsystems

---
 .../Topology/Compactness/CompactSystem.lean   | 373 ++++++++++++++++++
 1 file changed, 373 insertions(+)
 create mode 100644 Mathlib/Topology/Compactness/CompactSystem.lean

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
new file mode 100644
index 00000000000000..e18327e6ecdcb0
--- /dev/null
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -0,0 +1,373 @@
+/-
+Copyright (c) 2023 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne, Peter Pfaffelhuber
+-/
+import Mathlib.Topology.Compactness.Compact
+
+open Set
+
+section definition
+
+variable {α : Type*} {p : Set α → Prop} {C : ℕ → Set α}
+
+/-- 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. -/
+def IsCompactSystem (p : Set α → Prop) : Prop :=
+  ∀ C : ℕ → Set α, (∀ i, p (C i)) → ⋂ i, C i = ∅ → ∃ (n : ℕ), ⋂ i ≤ n, C i = ∅
+
+/-- In a compact system, given a countable family with empty intersection, we choose a finite
+subfamily with empty intersection-/
+noncomputable
+def IsCompactSystem.max_of_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i))
+    (hC_empty : ⋂ i, C i = ∅) : ℕ :=
+  (hp C hC hC_empty).choose
+
+lemma IsCompactSystem.iInter_eq_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i))
+    (hC_empty : ⋂ i, C i = ∅) :
+    ⋂ i ≤ hp.max_of_empty hC hC_empty, C i = ∅ :=
+  (hp C hC hC_empty).choose_spec
+
+
+
+
+example (i n : ℕ) : i ∈ Finset.range (n + 1) ↔ i ≤ n := by exact Finset.mem_range_succ_iff
+
+example (n : ℕ) : { i // i < n+1} = {i // i ≤ n} := by
+    simp_rw [Nat.lt_add_one_iff]
+
+example (i n : ℕ) : i < n+1 ↔ i ≤ n := by exact Nat.lt_add_one_iff
+
+example (C : ℕ → Set α) (n : ℕ) : ⋂ i < n+1, C i = ⋂ i ≤ n, C i :=
+  by simp_rw [Nat.lt_add_one_iff]
+
+example (n : ℕ) : (Finset.range (n + 1)).Nonempty := by exact Finset.nonempty_range_succ
+
+example (C : ℕ → Set α) (s : Finset ℕ) (hs : s = ∅): ⋂ i ∈ s, C i = ∅ := by apply?
+
+lemma iInter_empty_iff (C : ℕ → Set α) : (∃ n : ℕ, ⋂ i ≤ n, C i = ∅) ↔
+    (∃ (s : Finset ℕ) (hs : s.Nonempty), ⋂ i ∈ s, C i = ∅) := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · obtain ⟨n, hn⟩ := h
+    use (Finset.range (n + 1)), Finset.nonempty_range_succ
+    simp_rw [Finset.mem_range_succ_iff]
+    exact hn
+  · obtain ⟨s, hs1, hs⟩ := h
+    use (s.max' hs1)
+
+
+    sorry
+
+    simp_rw [← Finset.mem_range_succ_iff]
+
+    sorry
+
+  sorry
+
+
+theorem IsCompactSystem.iff_le : (IsCompactSystem p) ↔ ∀ C : ℕ → Set α, (∀ i, p (C i)) ↔
+    ⋂ i, C i = ∅ → ∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅ := by
+  sorry
+
+
+theorem IsCompactSystem.iff_mono : (IsCompactSystem p) ↔ ∀ (C : ℕ → Set α) (h : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) → ⋂ i, C i = ∅ →
+      ∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅ := by
+    rw [IsCompactSystem.iff_le]
+    refine ⟨fun h ↦ fun C _ i ↦ h C i, fun h C ↦ ?_⟩
+    let D := fun n ↦ ⋂ i ≤ n, C i
+    have h' := h C
+    have h1 : ∀ n, ⋂ i ≤ n, D i = ⋂ i ≤ n, C i := by sorry -- exact fun n ↦ Eq.symm biInter_le_eq_iInter
+    have h1' : ⋂ i, D i = ⋂ i, C i := by exact biInter_le_eq_iInter
+    have h2 : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) D := by
+      refine directed_of_isDirected_le ?_
+      intro i j hij
+      simp [D]
+      sorry
+    have h3 : ∀ (i : ℕ), p (D i) := by sorry
+    intro i hi
+    obtain h5 := h D h2 h3 (h1' ▸  hi)
+    rcases h5 with ⟨s, hs⟩
+    use Finset.range (s.max' ?_)
+
+    sorry
+
+
+
+    refine ⟨h D h2 h3 hi (h1' ▸  hi)⟩
+    simp_rw [← h1]
+    -- have h3 :
+    sorry
+    apply fun C i ↦ h C _ i
+
+    · sorry
+    -- refine ⟨?_, fun h_↦ h ⟩
+
+    sorry
+≤
+end definition
+
+/--
+section Compact
+
+variable {α : Type*} [TopologicalSpace α]
+
+theorem IsCompact.isCompactSystem : IsCompactSystem {s // IsCompact s} := by
+  simp [IsCompactSystem]
+
+  sorry
+
+
+end Compact
+
+section ClosedCompactCylinders
+
+/-! We prove that the `closedCompactCylinders` are a compact system. -/
+
+variable {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i)] {s : ℕ → Set (Π i, α i)}
+
+local notation "Js" => closedCompactCylinders.finset
+local notation "As" => closedCompactCylinders.set
+
+section AllProj
+
+/-- All indices in `ι` that are constrained by the condition `∀ n, s n ∈ closedCompactCylinders α`.
+That is, the union of all indices in the bases of the cylinders. -/
+def allProj (hs : ∀ n, s n ∈ closedCompactCylinders α) : Set ι := ⋃ n, Js (hs n)
+
+theorem subset_allProj (hs : ∀ n, s n ∈ closedCompactCylinders α) (n : ℕ) :
+    ↑(Js (hs n)) ⊆ allProj hs :=
+  subset_iUnion (fun i ↦ (Js (hs i) : Set ι)) n
+
+theorem exists_nat_proj (hs : ∀ n, s n ∈ closedCompactCylinders α) (i : ι) (hi : i ∈ allProj hs) :
+    ∃ n, i ∈ Js (hs n) := by
+  simpa only [allProj, mem_iUnion, Finset.mem_coe] using hi
+
+open Classical in
+/-- The smallest `n` such that `i ∈ Js (hs n)`. That is, the first `n` such that `i` belongs to the
+finset defining the cylinder for `s n`. -/
+noncomputable def indexProj (hs : ∀ n, s n ∈ closedCompactCylinders α) (i : allProj hs) : ℕ :=
+  Nat.find (exists_nat_proj hs i i.2)
+
+open Classical in
+theorem mem_indexProj (hs : ∀ n, s n ∈ closedCompactCylinders α) (i : allProj hs) :
+    (i : ι) ∈ Js (hs (indexProj hs i)) :=
+  Nat.find_spec (exists_nat_proj hs i i.2)
+
+open Classical in
+theorem indexProj_le (hs : ∀ n, s n ∈ closedCompactCylinders α) (n : ℕ) (i : Js (hs n)) :
+    indexProj hs ⟨i, subset_allProj hs n i.2⟩ ≤ n :=
+  Nat.find_le i.2
+
+lemma surjective_proj_allProj [∀ i, Nonempty (α i)] (hs : ∀ n, s n ∈ closedCompactCylinders α) :
+    Function.Surjective (fun (f : (Π i, α i)) (i : allProj hs) ↦ f (i : ι)) := by
+  intro y
+  let x := (inferInstance : Nonempty (Π i, α i)).some
+  classical
+  refine ⟨fun i ↦ if hi : i ∈ allProj hs then y ⟨i, hi⟩ else x i, ?_⟩
+  ext i
+  simp only [Subtype.coe_prop, dite_true]
+
+end AllProj
+
+section projCylinder
+
+/-- Given a countable family of closed cylinders, consider one of them as depending only on
+the countably many coordinates that appear in all of them. -/
+def projCylinder (hs : ∀ n, s n ∈ closedCompactCylinders α) (n : ℕ) :
+    Set (∀ i : allProj hs, α i) :=
+  (fun (f : ∀ i : allProj hs, α i) (i : Js (hs n)) ↦ f ⟨i, subset_allProj hs _ i.2⟩) ⁻¹' (As (hs n))
+
+lemma mem_projCylinder (hs : ∀ n, s n ∈ closedCompactCylinders α) (n : ℕ)
+    (x : ∀ i : allProj hs, α i) :
+    x ∈ projCylinder hs n ↔ (fun (i : Js (hs n)) ↦ x ⟨i, subset_allProj hs _ i.2⟩) ∈ As (hs n) := by
+  simp only [projCylinder, mem_preimage]
+
+theorem preimage_projCylinder (hs : ∀ n, s n ∈ closedCompactCylinders α) (n : ℕ) :
+    (fun (f : ∀ i, α i) (i : allProj hs) ↦ f i) ⁻¹' (projCylinder hs n) = s n := by
+  conv_rhs => rw [closedCompactCylinders.eq_cylinder (hs n)]
+  rfl
+
+lemma nonempty_projCylinder (hs : ∀ n, s n ∈ closedCompactCylinders α)
+    (n : ℕ) (hs_nonempty : (s n).Nonempty) :
+    (projCylinder hs n).Nonempty := by
+  rw [← preimage_projCylinder hs n] at hs_nonempty
+  exact nonempty_of_nonempty_preimage hs_nonempty
+
+lemma nonempty_projCylinder_iff [∀ i, Nonempty (α i)]
+    (hs : ∀ n, s n ∈ closedCompactCylinders α) (n : ℕ) :
+    (projCylinder hs n).Nonempty ↔ (s n).Nonempty := by
+  refine ⟨fun h ↦ ?_, nonempty_projCylinder hs n⟩
+  obtain ⟨x, hx⟩ := h
+  rw [mem_projCylinder] at hx
+  rw [closedCompactCylinders.eq_cylinder (hs n), MeasureTheory.cylinder]
+  refine Set.Nonempty.preimage ?_ ?_
+  · exact ⟨_, hx⟩
+  · intro y
+    let x := (inferInstance : Nonempty (∀ i, α i)).some
+    classical
+    refine ⟨fun i ↦ if hi : i ∈ Js (hs n) then y ⟨i, hi⟩ else x i, ?_⟩
+    ext i
+    simp only [Finset.restrict_def, Finset.coe_mem, dite_true]
+
+theorem isClosed_projCylinder
+    (hs : ∀ n, s n ∈ closedCompactCylinders α) (hs_closed : ∀ n, IsClosed (As (hs n))) (n : ℕ) :
+    IsClosed (projCylinder hs n) :=
+  (hs_closed n).preimage (by exact continuous_pi (fun i ↦ continuous_apply _))
+
+end projCylinder
+
+section piCylinderSet
+
+open Classical in
+/-- Given countably many closed compact cylinders, the product set which, in each relevant
+coordinate, is the projection of the first cylinder for which this coordinate is relevant. -/
+def piCylinderSet (hs : ∀ n, s n ∈ closedCompactCylinders α) :
+    Set (∀ i : allProj hs, α i) :=
+  {x : ∀ i : allProj hs, α i |
+    ∀ i, x i ∈ (fun a : ∀ j : Js (hs (indexProj hs i)), α j ↦ a ⟨i, mem_indexProj hs i⟩) ''
+      (As (hs (indexProj hs i)))}
+
+lemma mem_piCylinderSet (hs : ∀ n, s n ∈ closedCompactCylinders α)
+    (x : ∀ i : allProj hs, α i) :
+    x ∈ piCylinderSet hs ↔
+    ∀ i, x i ∈ (fun a : ∀ j : Js (hs (indexProj hs i)), α j ↦ a ⟨i, mem_indexProj hs i⟩) ''
+      (As (hs (indexProj hs i))) := by
+  simp only [piCylinderSet, mem_image, Subtype.forall, mem_setOf_eq]
+
+theorem isCompact_piCylinderSet (hs : ∀ n, s n ∈ closedCompactCylinders α) :
+    IsCompact (piCylinderSet hs) :=
+  isCompact_pi_infinite fun _ ↦
+    (closedCompactCylinders.isCompact (hs _)).image (continuous_apply _)
+
+theorem piCylinderSet_eq_pi_univ (hs : ∀ n, s n ∈ closedCompactCylinders α) :
+    piCylinderSet hs =
+      pi univ fun i ↦
+        (fun a : ∀ j : Js (hs (indexProj hs i)), α j ↦ a ⟨i, mem_indexProj hs i⟩) ''
+          (As (hs (indexProj hs i))) := by
+  ext; simp only [piCylinderSet, mem_univ_pi]; rfl
+
+theorem isClosed_piCylinderSet (hs : ∀ n, s n ∈ closedCompactCylinders α) :
+    IsClosed (piCylinderSet hs) := by
+  rw [piCylinderSet_eq_pi_univ]
+  exact isClosed_set_pi fun i _ ↦ IsClosed.isClosed_image_restrict_singleton _
+    (closedCompactCylinders.isCompact (hs _)) (closedCompactCylinders.isClosed (hs _))
+
+theorem nonempty_piCylinderSet (hs : ∀ n, s n ∈ closedCompactCylinders α)
+    (hs_nonempty : ∀ i, (s i).Nonempty) :
+    (piCylinderSet hs).Nonempty := by
+  have hs_nonempty' i : (As (hs i)).Nonempty := by
+    specialize hs_nonempty i
+    rw [closedCompactCylinders.eq_cylinder (hs i)] at hs_nonempty
+    exact nonempty_of_nonempty_preimage hs_nonempty
+  let b i := (hs_nonempty' (indexProj hs i)).some
+  have hb_mem i : b i ∈ As (hs (indexProj hs i)) := (hs_nonempty' (indexProj hs i)).choose_spec
+  let a : ∀ i : allProj hs, α i := fun i ↦ b i ⟨i, mem_indexProj hs i⟩
+  refine ⟨a, ?_⟩
+  simp only [piCylinderSet, mem_image, SetCoe.forall, mem_setOf_eq]
+  exact fun j hj ↦ ⟨b ⟨j, hj⟩, hb_mem _, rfl⟩
+
+end piCylinderSet
+
+theorem iInter_subset_piCylinderSet (hs : ∀ n, s n ∈ closedCompactCylinders α) :
+    (⋂ n, projCylinder hs n) ⊆ piCylinderSet hs := by
+  intro x hx
+  rw [mem_iInter] at hx
+  rw [mem_piCylinderSet]
+  intro i
+  specialize hx (indexProj hs i)
+  rw [mem_projCylinder] at hx
+  exact ⟨fun i : Js (hs (indexProj hs i)) ↦ x ⟨i, subset_allProj hs _ i.2⟩, hx, rfl⟩
+
+theorem nonempty_iInter_projCylinder_inter_piCylinderSet (hs : ∀ n, s n ∈ closedCompactCylinders α)
+    (hs_nonempty : ∀ i, (s i).Nonempty)
+    (h_nonempty : ∀ n, (⋂ i ≤ n, projCylinder hs i).Nonempty) (n : ℕ) :
+    ((⋂ i ≤ n, projCylinder hs i) ∩ piCylinderSet hs).Nonempty := by
+  obtain ⟨x, hx⟩ := nonempty_piCylinderSet hs hs_nonempty
+  obtain ⟨y, hy⟩ := h_nonempty n
+  let z := fun i : allProj hs ↦ if indexProj hs i ≤ n then y i else x i
+  refine ⟨z, mem_inter ?_ ?_⟩
+  · simp only [mem_iInter, mem_projCylinder]
+    intro i hi
+    have : (fun j : Js (hs i) ↦
+          ite (indexProj hs ⟨j, subset_allProj hs i j.2⟩ ≤ n) (y ⟨j, subset_allProj hs i j.2⟩)
+            (x ⟨j, subset_allProj hs i j.2⟩)) =
+        fun j : Js (hs i) ↦ y ⟨j, subset_allProj hs i j.2⟩ := by
+      ext j
+      rw [if_pos]
+      refine le_trans (le_of_eq ?_) ((indexProj_le hs i j).trans hi)
+      congr
+    rw [this]
+    have hyi : y ∈ projCylinder hs i := by
+      suffices ⋂ j ≤ n, projCylinder hs j ⊆ projCylinder hs i by exact this hy
+      exact biInter_subset_of_mem hi
+    rwa [mem_projCylinder] at hyi
+  · rw [mem_piCylinderSet]
+    intro i
+    by_cases hi_le : indexProj hs i ≤ n
+    · let m := indexProj hs i
+      have hy' : y ∈ projCylinder hs m := by
+        suffices ⋂ j ≤ n, projCylinder hs j ⊆ projCylinder hs m by exact this hy
+        exact biInter_subset_of_mem hi_le
+      rw [mem_projCylinder] at hy'
+      refine ⟨fun j ↦ y ⟨j, subset_allProj hs _ j.2⟩, hy', ?_⟩
+      simp_rw [z, if_pos hi_le]
+    · rw [mem_piCylinderSet] at hx
+      specialize hx i
+      obtain ⟨x', hx'_mem, hx'_eq⟩ := hx
+      refine ⟨x', hx'_mem, ?_⟩
+      simp_rw [z, if_neg hi_le]
+      exact hx'_eq
+
+theorem nonempty_iInter_projCylinder (hs : ∀ n, s n ∈ closedCompactCylinders α)
+    (hs_nonempty : ∀ i, (s i).Nonempty)
+    (h_nonempty : ∀ n, (⋂ i ≤ n, projCylinder hs i).Nonempty) :
+    (⋂ i, projCylinder hs i).Nonempty := by
+  suffices ((⋂ i, projCylinder hs i) ∩ piCylinderSet hs).Nonempty by
+    rwa [inter_eq_left.mpr (iInter_subset_piCylinderSet hs)] at this
+  have : (⋂ n, projCylinder hs n) = (⋂ n, ⋂ i ≤ n, projCylinder hs i) := by
+    ext x
+    simp only [mem_iInter]
+    exact ⟨fun h i j _ ↦ h j, fun h i ↦ h i i le_rfl⟩
+  rw [this, iInter_inter]
+  have h_closed : ∀ n, IsClosed (⋂ i ≤ n, projCylinder hs i) :=
+    fun n ↦ isClosed_biInter (fun i _ ↦ isClosed_projCylinder hs
+      (fun n ↦ (closedCompactCylinders.isClosed (hs n))) i)
+  refine IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
+    (fun n ↦ (⋂ i ≤ n, projCylinder hs i) ∩ piCylinderSet hs) ?_ ?_ ?_ ?_
+  · refine fun i ↦ inter_subset_inter ?_ subset_rfl
+    simp_rw [Set.biInter_le_succ]
+    exact inter_subset_left
+  · exact fun n ↦ nonempty_iInter_projCylinder_inter_piCylinderSet hs hs_nonempty h_nonempty n
+  · exact (isCompact_piCylinderSet hs).inter_left (h_closed _)
+  · exact fun n ↦ IsClosed.inter (h_closed n) (isClosed_piCylinderSet hs)
+
+lemma exists_finset_iInter_projCylinder_eq_empty [∀ i, Nonempty (α i)]
+    (hs : ∀ n, s n ∈ closedCompactCylinders α) (h : ⋂ n, projCylinder hs n = ∅) :
+    ∃ t : Finset ℕ, (⋂ i ∈ t, projCylinder hs i) = ∅ := by
+  by_contra! h_nonempty
+  refine absurd h (Set.Nonempty.ne_empty ?_)
+  refine nonempty_iInter_projCylinder hs (fun i ↦ ?_) (fun n ↦ ?_)
+  · specialize h_nonempty {i}
+    simp only [Finset.mem_singleton, iInter_iInter_eq_left, ne_eq] at h_nonempty
+    rwa [nonempty_projCylinder_iff] at h_nonempty
+  · specialize h_nonempty (Finset.range (n + 1))
+    simp only [Finset.mem_range, ne_eq, Nat.lt_succ_iff] at h_nonempty
+    exact h_nonempty
+
+/-- The `closedCompactCylinders` are a compact system. -/
+theorem isCompactSystem_closedCompactCylinders : IsCompactSystem (closedCompactCylinders α) := by
+  intro s hs h
+  by_cases hα : ∀ i, Nonempty (α i)
+  swap; · exact ⟨∅, by simpa [not_nonempty_iff] using hα⟩
+  have h' : ⋂ n, projCylinder hs n = ∅ := by
+    simp_rw [← preimage_projCylinder hs, ← preimage_iInter] at h
+    have h_surj : Function.Surjective (fun (f : (∀ i, α i)) (i : allProj hs) ↦ f (i : ι)) :=
+      surjective_proj_allProj hs
+    rwa [← not_nonempty_iff_eq_empty, ← Function.Surjective.nonempty_preimage h_surj,
+      not_nonempty_iff_eq_empty]
+  obtain ⟨t, ht⟩ := exists_finset_iInter_projCylinder_eq_empty hs h'
+  refine ⟨t, ?_⟩
+  simp_rw [← preimage_projCylinder hs, ← preimage_iInter₂, ht, preimage_empty]
+
+end ClosedCompactCylinders
+-/

From 08d543caa8c9558a41e169f0b6b04d66790f0415 Mon Sep 17 00:00:00 2001
From: pfaffelh <p.p@stochastik.uni-freiburg.de>
Date: Thu, 13 Feb 2025 00:37:12 +0100
Subject: [PATCH 02/53] not there for compact

---
 .../Topology/Compactness/CompactSystem.lean   | 178 ++++++++++++------
 1 file changed, 122 insertions(+), 56 deletions(-)

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index e18327e6ecdcb0..201d039aacf6f7 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Peter Pfaffelhuber
 -/
 import Mathlib.Topology.Compactness.Compact
+import Mathlib.MeasureTheory.PiSystem
 
-open Set
+open Set Finset Nat
 
 section definition
 
@@ -29,7 +30,15 @@ lemma IsCompactSystem.iInter_eq_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C
   (hp C hC hC_empty).choose_spec
 
 
+example (i n : ℕ) : i < n+1 ↔ i ≤ n := by exact Nat.lt_add_one_iff
+
+lemma l1 (s : Finset ℕ) (hs : s.Nonempty) : s ⊆ Finset.range (s.max' hs + 1) := by
+  intro i hi
+  rw [Finset.mem_range, Nat.lt_add_one_iff]
+  exact s.le_max' i hi
 
+example (s : Finset ℕ) (hs : s.Nonempty) (i : ℕ) (hi : i ∈ s) : i ≤ s.max' hs := by
+  exact Finset.le_max' s i hi
 
 example (i n : ℕ) : i ∈ Finset.range (n + 1) ↔ i ≤ n := by exact Finset.mem_range_succ_iff
 
@@ -45,65 +54,122 @@ example (n : ℕ) : (Finset.range (n + 1)).Nonempty := by exact Finset.nonempty_
 
 example (C : ℕ → Set α) (s : Finset ℕ) (hs : s = ∅): ⋂ i ∈ s, C i = ∅ := by apply?
 
-lemma iInter_empty_iff (C : ℕ → Set α) : (∃ n : ℕ, ⋂ i ≤ n, C i = ∅) ↔
-    (∃ (s : Finset ℕ) (hs : s.Nonempty), ⋂ i ∈ s, C i = ∅) := by
-  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-  · obtain ⟨n, hn⟩ := h
-    use (Finset.range (n + 1)), Finset.nonempty_range_succ
+@[simp]
+lemma iInter_empty_iff [Inhabited α] {C : ℕ → Set α} : (∃ n : ℕ, ⋂ i ≤ n, C i = ∅) ↔
+    (∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅) := by
+  refine ⟨fun ⟨n, hn⟩ ↦ ?_, fun ⟨s, hs⟩ ↦ ?_⟩
+  · use (Finset.range (n + 1))
     simp_rw [Finset.mem_range_succ_iff]
     exact hn
-  · obtain ⟨s, hs1, hs⟩ := h
-    use (s.max' hs1)
-
-
-    sorry
-
-    simp_rw [← Finset.mem_range_succ_iff]
-
-    sorry
-
-  sorry
-
-
-theorem IsCompactSystem.iff_le : (IsCompactSystem p) ↔ ∀ C : ℕ → Set α, (∀ i, p (C i)) ↔
-    ⋂ i, C i = ∅ → ∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅ := by
-  sorry
-
-
-theorem IsCompactSystem.iff_mono : (IsCompactSystem p) ↔ ∀ (C : ℕ → Set α) (h : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) → ⋂ i, C i = ∅ →
-      ∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅ := by
-    rw [IsCompactSystem.iff_le]
-    refine ⟨fun h ↦ fun C _ i ↦ h C i, fun h C ↦ ?_⟩
-    let D := fun n ↦ ⋂ i ≤ n, C i
-    have h' := h C
-    have h1 : ∀ n, ⋂ i ≤ n, D i = ⋂ i ≤ n, C i := by sorry -- exact fun n ↦ Eq.symm biInter_le_eq_iInter
-    have h1' : ⋂ i, D i = ⋂ i, C i := by exact biInter_le_eq_iInter
-    have h2 : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) D := by
-      refine directed_of_isDirected_le ?_
-      intro i j hij
-      simp [D]
-      sorry
-    have h3 : ∀ (i : ℕ), p (D i) := by sorry
+  · have h2 : s.Nonempty := by
+      rw [s.nonempty_iff_ne_empty]
+      intro h
+      rw [h] at hs
+      simp only [Finset.not_mem_empty, iInter_of_empty, iInter_univ, Set.univ_eq_empty_iff,
+        not_isEmpty_of_nonempty] at hs
+    use (s.max' h2)
+    have h : ⋂ i, ⋂ (_ : i ≤ s.max' h2), C i ⊆ ⋂ i ∈ s, C i := by
+      simp_rw [← Finset.mem_range_succ_iff]
+      exact biInter_mono (l1 s h2) (fun _ _ ⦃a_1⦄ a ↦ a)
+    exact subset_empty_iff.mp <| le_trans h hs.le
+
+theorem IsCompactSystem.iff_le [Inhabited α] : (IsCompactSystem p) ↔
+    (∀ C : ℕ → Set α, (∀ i, p (C i)) → ⋂ i, C i = ∅ → ∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅) := by
+  refine ⟨fun h C hp he ↦ ?_, fun h C hp he ↦ ?_ ⟩
+  · apply iInter_empty_iff.mp <| h C hp he
+  · apply iInter_empty_iff.mpr <| h C hp he
+
+
+
+
+theorem biInter_decumulate (s : ℕ → Set α) (n : ℕ):
+    ⋂ x ≤ n, ⋂ y ≤ x, s y = ⋂ y ≤ n, s y := by
+  apply Set.Subset.antisymm
+  · apply iInter_mono
+    intro z x hx
+    simp at hx
+    simp only [mem_iInter]
+    exact fun h ↦ hx h z <| Nat.le_refl z
+  · simp only [subset_iInter_iff]
+    intro i hi x hx
+    refine biInter_subset_of_mem ?_
+    simp only [le_eq]
+    exact le_trans hx hi
+
+theorem decumulate_succ (s : ℕ → Set α) (n : ℕ) :
+    ⋂ i ≤ n + 1, s i = (⋂ i ≤ n, s i) ∩ s (n + 1) := by
+  ext x
+  refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
+  · simp only [mem_inter_iff, mem_iInter] at *
+    exact ⟨fun i hi ↦ hx i <| le_trans hi <| le_add_right n 1, hx (n + 1) <| Nat.le_refl (n + 1)⟩
+  · simp only [mem_inter_iff, mem_iInter] at *
     intro i hi
-    obtain h5 := h D h2 h3 (h1' ▸  hi)
-    rcases h5 with ⟨s, hs⟩
-    use Finset.range (s.max' ?_)
-
-    sorry
-
-
-
-    refine ⟨h D h2 h3 hi (h1' ▸  hi)⟩
-    simp_rw [← h1]
-    -- have h3 :
-    sorry
-    apply fun C i ↦ h C _ i
-
-    · sorry
-    -- refine ⟨?_, fun h_↦ h ⟩
+    by_cases h : i ≤ n
+    · exact hx.1 i h
+    · simp only [not_le] at h
+      exact Nat.le_antisymm hi h ▸ hx.2
+
+theorem iInter_decumulate (s : ℕ → Set α) (n : ℕ): ⋂ x, ⋂ y ≤ x, s y = ⋂ y, s y := by
+  apply Set.Subset.antisymm
+  · apply iInter_mono
+    intro z x hx
+    simp at hx
+    apply hx z <| Nat.le_refl z
+  · simp only [subset_iInter_iff]
+    intro i x hx
+    exact iInter_subset_of_subset x fun ⦃a⦄ a ↦ a
+
+def IsPiSystem' (C : Set (Set α)) := ∀ s ∈ C, ∀ t ∈ C, s ∩ t ∈ C
+
+lemma prime (C : Set (Set α)) (hC : ∅ ∈ C) : (IsPiSystem C) ↔ (IsPiSystem' C) := by
+  refine ⟨fun h s hs t ht ↦ ?_, fun h s hs t ht _ ↦ h s hs t ht⟩
+  by_cases h' : (s ∩ t).Nonempty
+  · exact h s hs t ht h'
+  · push_neg at h'
+    exact h' ▸ hC
+
+example (C D : ℕ → Set α) (n : ℕ) (hCD : C = D) : ⋂ i ≤ n, C i = ⋂ i ≤ n, D i := by
+  exact iInter₂_congr fun i j ↦ congrFun hCD i
+
+lemma l2 (C : Set (Set α)) (hC : IsPiSystem' C) (s : ℕ → Set α) (hs : ∀ n, s n ∈ C) (n : ℕ) :
+    ⋂ i ≤ n, s i ∈ C :=  by
+  induction n with
+  | zero =>
+    simp only [le_zero_eq, iInter_iInter_eq_left]
+    exact hs 0
+  | succ n hn =>
+    rw [decumulate_succ s n]
+    exact hC (⋂ i, ⋂ (_ : i ≤ n), s i) hn (s (n + 1)) (hs (n + 1))
+
+theorem IsCompactSystem.iff_mono [Inhabited α] (hpi : IsPiSystem' p) : (IsCompactSystem p) ↔
+    (∀ (C : ℕ → Set α) (h : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
+      ⋂ i, C i = ∅ → ∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅) := by
+  rw [IsCompactSystem.iff_le]
+  refine ⟨fun h ↦ fun C _ i ↦ h C i, fun h C ↦ ?_⟩
+  let D := fun n ↦ ⋂ i ≤ n, C i
+  have h' := h C
+  have h1 (n : ℕ) : ⋂ i ≤ n, D i = ⋂ i ≤ n, C i := biInter_decumulate C n
+  have h1' : ⋂ i, D i = ⋂ i, C i := by exact biInter_le_eq_iInter
+  have h2 : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) D := by
+    refine directed_of_isDirected_le ?_
+    intro i j hij
+    simp [D]
+    intro k hk
+    refine biInter_subset_of_mem ?_
+    exact le_trans hk hij
+  intro hi hi'
+  have h3 (i : ℕ) : p (D i) := by
+    simp [D, hpi]
+    obtain h4 := l2 {s : Set α | p s} hpi C
+    obtain h5 := h4 hi i
+    exact h5
+  obtain h5 := h D h2 h3 (h1' ▸  hi')
+  obtain h6 := h D h2
+  rw [← iInter_empty_iff] at *
+  rcases h5 with ⟨n, hn⟩
+  use n
+  rwa [← h1 n]
 
-    sorry
-≤
 end definition
 
 /--

From f69f095e24a44d328866f4dbe100cde4e3385846 Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@pc.fritz.box>
Date: Fri, 14 Feb 2025 00:35:53 +0100
Subject: [PATCH 03/53] not done yet

---
 .../Topology/Compactness/CompactSystem.lean   | 49 +++++++++++++++++--
 1 file changed, 46 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 201d039aacf6f7..61be3ce9729976 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -29,6 +29,21 @@ lemma IsCompactSystem.iInter_eq_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C
     ⋂ i ≤ hp.max_of_empty hC hC_empty, C i = ∅ :=
   (hp C hC hC_empty).choose_spec
 
+def IsCompactSystem' (p : Set α → Prop) : Prop :=
+  ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ (n : ℕ), (⋂ i ≤ n, C i).Nonempty) → (⋂ i, C i).Nonempty
+
+theorem IsCompactSystem_iff_IsCompactSystem' (p : Set α → Prop) :
+    IsCompactSystem p ↔ IsCompactSystem' p := by
+  refine ⟨fun h C hC hn ↦ ?_, fun h C hC ↦ ?_⟩
+  · have h2 := h C hC
+    rw [← not_imp_not] at h2
+    push_neg at h2
+    simp_rw [Set.nonempty_iff_ne_empty] at *
+    exact h2 hn
+  · have h2 := h C hC
+    rw [← not_imp_not] at h2
+    push_neg at h2
+    exact h2
 
 example (i n : ℕ) : i < n+1 ↔ i ≤ n := by exact Nat.lt_add_one_iff
 
@@ -141,8 +156,11 @@ lemma l2 (C : Set (Set α)) (hC : IsPiSystem' C) (s : ℕ → Set α) (hs : ∀
     rw [decumulate_succ s n]
     exact hC (⋂ i, ⋂ (_ : i ≤ n), s i) hn (s (n + 1)) (hs (n + 1))
 
+lemma l3 (C : ℕ → Set α) (hC : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) :
+  ∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅ ↔ ∃ n, C n = ∅ := by sorry
+
 theorem IsCompactSystem.iff_mono [Inhabited α] (hpi : IsPiSystem' p) : (IsCompactSystem p) ↔
-    (∀ (C : ℕ → Set α) (h : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
+    (∀ (C : ℕ → Set α) (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
       ⋂ i, C i = ∅ → ∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅) := by
   rw [IsCompactSystem.iff_le]
   refine ⟨fun h ↦ fun C _ i ↦ h C i, fun h C ↦ ?_⟩
@@ -170,21 +188,46 @@ theorem IsCompactSystem.iff_mono [Inhabited α] (hpi : IsPiSystem' p) : (IsCompa
   use n
   rwa [← h1 n]
 
+lemma l4 : (∀ (n : ℕ), (C n).Nonempty →
+  (⋂ i, C i).Nonempty) ↔ ((⋂ i, C i) = ∅ → ∃ (n : ℕ), (C n) = ∅) := by
+
+  sorry
+
+theorem IsCompactSystem.iff_mono' [Inhabited α] (hpi : IsPiSystem' p) : (IsCompactSystem p) ↔
+  ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
+    ∀ (n : ℕ), (C n).Nonempty →
+      (⋂ i, C i).Nonempty  := by
+  rw [IsCompactSystem.iff_mono hpi]
+  refine ⟨fun h1 h2 ↦ ?_, fun h1 h2 h3 h4 h5 ↦ ?_⟩
+  · sorry
+  · sorry
+
+
+
 end definition
 
-/--
 section Compact
 
 variable {α : Type*} [TopologicalSpace α]
 
-theorem IsCompact.isCompactSystem : IsCompactSystem {s // IsCompact s} := by
+theorem IsCompact.isCompactSystem {α : Type*} [Inhabited α] [TopologicalSpace α] :
+    IsCompactSystem (⋃ (s : Set α) (_ : IsCompact s), {s}) := by
+  have h : IsPiSystem' (⋃ (s : Set α) (_ : IsCompact s), {s}) := by sorry
+  rw [IsCompactSystem.iff_mono' h]
+  apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
+  -- IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
+  sorry
+
   simp [IsCompactSystem]
+  intro C hC h_empty
 
   sorry
 
 
+
 end Compact
 
+/--
 section ClosedCompactCylinders
 
 /-! We prove that the `closedCompactCylinders` are a compact system. -/

From cf6a0c475bd6a709563c72969147aea92ee7ddc6 Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Fri, 14 Feb 2025 14:32:10 +0100
Subject: [PATCH 04/53] found emptyset

---
 .../Topology/Compactness/CompactSystem.lean   | 51 ++++++++++++++-----
 1 file changed, 39 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 61be3ce9729976..1d96e1a369f179 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -195,7 +195,7 @@ lemma l4 : (∀ (n : ℕ), (C n).Nonempty →
 
 theorem IsCompactSystem.iff_mono' [Inhabited α] (hpi : IsPiSystem' p) : (IsCompactSystem p) ↔
   ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
-    ∀ (n : ℕ), (C n).Nonempty →
+    (∀ (n : ℕ), (C n).Nonempty) →
       (⋂ i, C i).Nonempty  := by
   rw [IsCompactSystem.iff_mono hpi]
   refine ⟨fun h1 h2 ↦ ?_, fun h1 h2 h3 h4 h5 ↦ ?_⟩
@@ -208,22 +208,49 @@ end definition
 
 section Compact
 
-variable {α : Type*} [TopologicalSpace α]
+variable {α : Type*}
 
-theorem IsCompact.isCompactSystem {α : Type*} [Inhabited α] [TopologicalSpace α] :
-    IsCompactSystem (⋃ (s : Set α) (_ : IsCompact s), {s}) := by
-  have h : IsPiSystem' (⋃ (s : Set α) (_ : IsCompact s), {s}) := by sorry
-  rw [IsCompactSystem.iff_mono' h]
-  apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
-  -- IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
-  sorry
+@[simp]
+lemma l5 (p : α → Prop) (s : α) : p s ↔ (s ∈ ⋃ (i : α) (_ : p i), {i}) := by
+  rw [Set.mem_iUnion₂]
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_ ⟩
+  · use s, h
+    simp only [mem_singleton_iff]
+  · obtain ⟨i, hi, h⟩ := h
+    simp only [mem_singleton_iff] at h
+    exact h ▸ hi
+
+lemma l6 (p q : α → Prop) (s : α) : (p s ∧ q s) ↔ (s ∈ ⋃ (i : α) (_ : p i) (_ : q i), {i}) := by
+  rw [Set.mem_iUnion₂]
+  simp_rw [mem_iUnion]
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_ ⟩
+  · use s, h.1, h.2
+    simp only [mem_singleton_iff]
+  · obtain ⟨i, hi, h1, h2⟩ := h
+    simp only [mem_singleton_iff] at h2
+    exact h2 ▸ ⟨hi, h1⟩
+
+lemma l7 (p : α → Prop) (s : α) : (s ∈ ⋃ (i : α) (_ : p i), {i}) ↔ (⋃ (i : α) (_ : p i), {i}) s:= by
+  rfl
 
-  simp [IsCompactSystem]
-  intro C hC h_empty
+variable {α : Type*} [TopologicalSpace α]
 
-  sorry
+example (p : α → Prop) (s : α) : (⋃ (i : α) (_ : p i), {i}) s ↔ p s := by
+  apply?
 
+theorem IsCompact.isCompactSystem {α : Type*} [Inhabited α] [TopologicalSpace α] :
+    IsCompactSystem (⋃ (s : Set α) (_ : IsCompact s) (_ : IsClosed s), {s}) := by
+  have h : IsPiSystem' (⋃ (s : Set α) (_ : IsCompact s) (_ : IsClosed s), {s}) := by
 
+    simp_rw [(l6 IsCompact IsClosed)]
+    sorry
+  rw [IsCompactSystem.iff_mono' h]
+  intro C hC h1 hn
+  have h1' (i : ℕ) : IsCompact (C i) ∧ IsClosed (C i):= by
+    rw [(l6 IsCompact IsClosed (C i))]
+    exact h1 i
+  exact IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed C hC hn
+    (fun i ↦ (h1' i).1) (fun i ↦ (h1' i).2)
 
 end Compact
 

From 5d99e0b1d97cbca86a9498f86ecccc4c94508a86 Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@pc.fritz.box>
Date: Sat, 15 Feb 2025 00:31:14 +0100
Subject: [PATCH 05/53] added mono

---
 .../Topology/Compactness/CompactSystem.lean   | 71 ++++++++++++++++---
 1 file changed, 61 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 1d96e1a369f179..303b6e7925ae91 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -88,6 +88,9 @@ lemma iInter_empty_iff [Inhabited α] {C : ℕ → Set α} : (∃ n : ℕ, ⋂ i
       exact biInter_mono (l1 s h2) (fun _ _ ⦃a_1⦄ a ↦ a)
     exact subset_empty_iff.mp <| le_trans h hs.le
 
+
+
+
 theorem IsCompactSystem.iff_le [Inhabited α] : (IsCompactSystem p) ↔
     (∀ C : ℕ → Set α, (∀ i, p (C i)) → ⋂ i, C i = ∅ → ∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅) := by
   refine ⟨fun h C hp he ↦ ?_, fun h C hp he ↦ ?_ ⟩
@@ -161,9 +164,44 @@ lemma l3 (C : ℕ → Set α) (hC : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2)
 
 theorem IsCompactSystem.iff_mono [Inhabited α] (hpi : IsPiSystem' p) : (IsCompactSystem p) ↔
     (∀ (C : ℕ → Set α) (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
-      ⋂ i, C i = ∅ → ∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅) := by
-  rw [IsCompactSystem.iff_le]
-  refine ⟨fun h ↦ fun C _ i ↦ h C i, fun h C ↦ ?_⟩
+      ⋂ i, C i = ∅ → ∃ (n : ℕ), C n = ∅) := by
+  have hs (C : ℕ → Set α) (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) : (∃ n, C n = ∅) ↔ (∃ n, ⋂ i ≤ n, C i = ∅) := by
+    refine ⟨fun h ↦ ?_, ?_⟩
+    · obtain ⟨n, hn⟩ := h
+      use n
+      by_cases hn' : n = 0
+      · rw [hn']
+        simp only [le_zero_eq, iInter_iInter_eq_left]
+        exact hn' ▸ hn
+      · obtain ⟨k, hk⟩ := exists_eq_succ_of_ne_zero hn'
+        rw [hk, decumulate_succ, ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
+    · have h3 (n : ℕ) : ∃ m, ⋂ i ≤ n, C i ⊇ C m := by
+        induction n with
+        | zero =>
+          use 0
+          simp
+        | succ n hn =>
+          obtain ⟨m, hm⟩ := hn
+          rw [decumulate_succ]
+          obtain ⟨k, hk⟩ := hd m (n+1)
+          simp at hk
+          use k
+          simp only [Set.subset_inter_iff]
+          exact ⟨le_trans hk.1 hm, hk.2⟩
+      rw [← not_imp_not]
+      push_neg
+      intro h n
+      obtain h2 := hd n (n + 1)
+      simp at h2
+      obtain ⟨m, hm⟩ := h3 n
+      exact Set.Nonempty.mono hm (h m)
+  -- rw [IsCompactSystem.iff_le]
+  refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C ↦ ?_⟩
+  · rw [hs C hdi]
+    exact h C hi
+  ·
+    sorry
+
   let D := fun n ↦ ⋂ i ≤ n, C i
   have h' := h C
   have h1 (n : ℕ) : ⋂ i ≤ n, D i = ⋂ i ≤ n, C i := biInter_decumulate C n
@@ -190,16 +228,23 @@ theorem IsCompactSystem.iff_mono [Inhabited α] (hpi : IsPiSystem' p) : (IsCompa
 
 lemma l4 : (∀ (n : ℕ), (C n).Nonempty →
   (⋂ i, C i).Nonempty) ↔ ((⋂ i, C i) = ∅ → ∃ (n : ℕ), (C n) = ∅) := by
-
   sorry
 
+example (P Q : Prop) : (P → Q) ↔ (¬ Q → ¬ P) := by exact Iff.symm not_imp_not
+
+
 theorem IsCompactSystem.iff_mono' [Inhabited α] (hpi : IsPiSystem' p) : (IsCompactSystem p) ↔
   ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
     (∀ (n : ℕ), (C n).Nonempty) →
       (⋂ i, C i).Nonempty  := by
-  rw [IsCompactSystem.iff_mono hpi]
-  refine ⟨fun h1 h2 ↦ ?_, fun h1 h2 h3 h4 h5 ↦ ?_⟩
-  · sorry
+  -- rw [IsCompactSystem.iff_mono hpi]
+  refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 h2 h3 h4 ↦ ?_⟩
+  · rw [← not_imp_not]
+    push_neg
+
+    refine h1 C h4
+    simp only [nonempty_iInter, not_exists, not_forall]
+    sorry
   · sorry
 
 
@@ -238,12 +283,16 @@ variable {α : Type*} [TopologicalSpace α]
 example (p : α → Prop) (s : α) : (⋃ (i : α) (_ : p i), {i}) s ↔ p s := by
   apply?
 
+example (x y : Set α) (hx : IsClosed x) (hy : IsClosed y) : IsClosed (x ∩ y) := by
+  exact IsClosed.inter hx hy
+
+
 theorem IsCompact.isCompactSystem {α : Type*} [Inhabited α] [TopologicalSpace α] :
     IsCompactSystem (⋃ (s : Set α) (_ : IsCompact s) (_ : IsClosed s), {s}) := by
   have h : IsPiSystem' (⋃ (s : Set α) (_ : IsCompact s) (_ : IsClosed s), {s}) := by
-
-    simp_rw [(l6 IsCompact IsClosed)]
-    sorry
+    intro x hx y hy
+    rw [← (l6 IsCompact IsClosed)] at *
+    exact ⟨IsCompact.inter_left hy.1 hx.2, IsClosed.inter hx.2 hy.2 ⟩
   rw [IsCompactSystem.iff_mono' h]
   intro C hC h1 hn
   have h1' (i : ℕ) : IsCompact (C i) ∧ IsClosed (C i):= by
@@ -252,6 +301,8 @@ theorem IsCompact.isCompactSystem {α : Type*} [Inhabited α] [TopologicalSpace
   exact IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed C hC hn
     (fun i ↦ (h1' i).1) (fun i ↦ (h1' i).2)
 
+
+
 end Compact
 
 /--

From dabe67daffe3920b4e9a1c265a892c318a3160fd Mon Sep 17 00:00:00 2001
From: pfaffelh <p.p@stochastik.uni-freiburg.de>
Date: Sat, 15 Feb 2025 01:18:20 +0100
Subject: [PATCH 06/53] compiles

---
 .../Topology/Compactness/CompactSystem.lean   | 141 ++++++++----------
 1 file changed, 62 insertions(+), 79 deletions(-)

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 303b6e7925ae91..2b6251c95d39de 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -67,8 +67,6 @@ example (C : ℕ → Set α) (n : ℕ) : ⋂ i < n+1, C i = ⋂ i ≤ n, C i :=
 
 example (n : ℕ) : (Finset.range (n + 1)).Nonempty := by exact Finset.nonempty_range_succ
 
-example (C : ℕ → Set α) (s : Finset ℕ) (hs : s = ∅): ⋂ i ∈ s, C i = ∅ := by apply?
-
 @[simp]
 lemma iInter_empty_iff [Inhabited α] {C : ℕ → Set α} : (∃ n : ℕ, ⋂ i ≤ n, C i = ∅) ↔
     (∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅) := by
@@ -127,7 +125,7 @@ theorem decumulate_succ (s : ℕ → Set α) (n : ℕ) :
     · simp only [not_le] at h
       exact Nat.le_antisymm hi h ▸ hx.2
 
-theorem iInter_decumulate (s : ℕ → Set α) (n : ℕ): ⋂ x, ⋂ y ≤ x, s y = ⋂ y, s y := by
+theorem iInter_decumulate (s : ℕ → Set α) : ⋂ x, ⋂ y ≤ x, s y = ⋂ y, s y := by
   apply Set.Subset.antisymm
   · apply iInter_mono
     intro z x hx
@@ -159,76 +157,64 @@ lemma l2 (C : Set (Set α)) (hC : IsPiSystem' C) (s : ℕ → Set α) (hs : ∀
     rw [decumulate_succ s n]
     exact hC (⋂ i, ⋂ (_ : i ≤ n), s i) hn (s (n + 1)) (hs (n + 1))
 
-lemma l3 (C : ℕ → Set α) (hC : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) :
-  ∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅ ↔ ∃ n, C n = ∅ := by sorry
+lemma l10 (C : ℕ → Set α) (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) :
+      (∃ n, C n = ∅) ↔ (∃ n, ⋂ i ≤ n, C i = ∅) := by
+  refine ⟨fun h ↦ ?_, ?_⟩
+  · obtain ⟨n, hn⟩ := h
+    use n
+    by_cases hn' : n = 0
+    · rw [hn']
+      simp only [le_zero_eq, iInter_iInter_eq_left]
+      exact hn' ▸ hn
+    · obtain ⟨k, hk⟩ := exists_eq_succ_of_ne_zero hn'
+      rw [hk, decumulate_succ, ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
+  · have h3 (n : ℕ) : ∃ m, ⋂ i ≤ n, C i ⊇ C m := by
+      induction n with
+      | zero =>
+        use 0
+        simp
+      | succ n hn =>
+        obtain ⟨m, hm⟩ := hn
+        rw [decumulate_succ]
+        obtain ⟨k, hk⟩ := hd m (n+1)
+        simp at hk
+        use k
+        simp only [Set.subset_inter_iff]
+        exact ⟨le_trans hk.1 hm, hk.2⟩
+    rw [← not_imp_not]
+    push_neg
+    intro h n
+    obtain h2 := hd n (n + 1)
+    simp at h2
+    obtain ⟨m, hm⟩ := h3 n
+    exact Set.Nonempty.mono hm (h m)
 
 theorem IsCompactSystem.iff_mono [Inhabited α] (hpi : IsPiSystem' p) : (IsCompactSystem p) ↔
-    (∀ (C : ℕ → Set α) (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
+    (∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
       ⋂ i, C i = ∅ → ∃ (n : ℕ), C n = ∅) := by
-  have hs (C : ℕ → Set α) (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) : (∃ n, C n = ∅) ↔ (∃ n, ⋂ i ≤ n, C i = ∅) := by
-    refine ⟨fun h ↦ ?_, ?_⟩
-    · obtain ⟨n, hn⟩ := h
-      use n
-      by_cases hn' : n = 0
-      · rw [hn']
-        simp only [le_zero_eq, iInter_iInter_eq_left]
-        exact hn' ▸ hn
-      · obtain ⟨k, hk⟩ := exists_eq_succ_of_ne_zero hn'
-        rw [hk, decumulate_succ, ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
-    · have h3 (n : ℕ) : ∃ m, ⋂ i ≤ n, C i ⊇ C m := by
-        induction n with
-        | zero =>
-          use 0
-          simp
-        | succ n hn =>
-          obtain ⟨m, hm⟩ := hn
-          rw [decumulate_succ]
-          obtain ⟨k, hk⟩ := hd m (n+1)
-          simp at hk
-          use k
-          simp only [Set.subset_inter_iff]
-          exact ⟨le_trans hk.1 hm, hk.2⟩
-      rw [← not_imp_not]
-      push_neg
-      intro h n
-      obtain h2 := hd n (n + 1)
-      simp at h2
-      obtain ⟨m, hm⟩ := h3 n
-      exact Set.Nonempty.mono hm (h m)
-  -- rw [IsCompactSystem.iff_le]
-  refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C ↦ ?_⟩
-  · rw [hs C hdi]
+  refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩
+  · rw [l10 C hdi]
     exact h C hi
-  ·
-    sorry
-
-  let D := fun n ↦ ⋂ i ≤ n, C i
-  have h' := h C
-  have h1 (n : ℕ) : ⋂ i ≤ n, D i = ⋂ i ≤ n, C i := biInter_decumulate C n
-  have h1' : ⋂ i, D i = ⋂ i, C i := by exact biInter_le_eq_iInter
-  have h2 : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) D := by
-    refine directed_of_isDirected_le ?_
-    intro i j hij
-    simp [D]
-    intro k hk
-    refine biInter_subset_of_mem ?_
-    exact le_trans hk hij
-  intro hi hi'
-  have h3 (i : ℕ) : p (D i) := by
-    simp [D, hpi]
-    obtain h4 := l2 {s : Set α | p s} hpi C
-    obtain h5 := h4 hi i
-    exact h5
-  obtain h5 := h D h2 h3 (h1' ▸  hi')
-  obtain h6 := h D h2
-  rw [← iInter_empty_iff] at *
-  rcases h5 with ⟨n, hn⟩
-  use n
-  rwa [← h1 n]
-
-lemma l4 : (∀ (n : ℕ), (C n).Nonempty →
-  (⋂ i, C i).Nonempty) ↔ ((⋂ i, C i) = ∅ → ∃ (n : ℕ), (C n) = ∅) := by
-  sorry
+  · let D := fun n ↦ ⋂ i ≤ n, C i
+    have h' := h C
+    have h8 (n : ℕ) : ⋂ i ≤ n, D i = ⋂ i ≤ n, C i := biInter_decumulate C n
+    have h1' : ⋂ i, D i = ⋂ i, C i := by exact biInter_le_eq_iInter
+    have h9 : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) D := by
+      refine directed_of_isDirected_le ?_
+      intro i j hij
+      simp [D]
+      intro k hk
+      refine biInter_subset_of_mem ?_
+      exact le_trans hk hij
+    have h3 (i : ℕ) : p (D i) := by
+      simp [D, hpi]
+      obtain h4 := l2 {s : Set α | p s} hpi C
+      obtain h5 := h4 h1 i
+      exact h5
+    obtain h5 := h D h9 h3 (h1' ▸  h2)
+    obtain h6 := h D h9
+    rcases h5 with ⟨n, hn⟩
+    use n
 
 example (P Q : Prop) : (P → Q) ↔ (¬ Q → ¬ P) := by exact Iff.symm not_imp_not
 
@@ -237,15 +223,15 @@ theorem IsCompactSystem.iff_mono' [Inhabited α] (hpi : IsPiSystem' p) : (IsComp
   ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
     (∀ (n : ℕ), (C n).Nonempty) →
       (⋂ i, C i).Nonempty  := by
-  -- rw [IsCompactSystem.iff_mono hpi]
-  refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 h2 h3 h4 ↦ ?_⟩
+  rw [IsCompactSystem.iff_mono hpi]
+  refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 ↦ ?_⟩
   · rw [← not_imp_not]
     push_neg
-
-    refine h1 C h4
-    simp only [nonempty_iInter, not_exists, not_forall]
-    sorry
-  · sorry
+    exact h1 C h3 h4
+  · intro s
+    rw [← not_imp_not]
+    push_neg
+    exact h1 C h3 s
 
 
 
@@ -280,9 +266,6 @@ lemma l7 (p : α → Prop) (s : α) : (s ∈ ⋃ (i : α) (_ : p i), {i}) ↔ (
 
 variable {α : Type*} [TopologicalSpace α]
 
-example (p : α → Prop) (s : α) : (⋃ (i : α) (_ : p i), {i}) s ↔ p s := by
-  apply?
-
 example (x y : Set α) (hx : IsClosed x) (hy : IsClosed y) : IsClosed (x ∩ y) := by
   exact IsClosed.inter hx hy
 

From 911f11273f58f44e03d50e4a960be97c6580664e Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Sat, 15 Feb 2025 13:32:58 +0100
Subject: [PATCH 07/53] dissipate

---
 Mathlib/Data/Set/Dissipate.lean               | 109 ++++++++++++++++++
 .../Topology/Compactness/CompactSystem.lean   |   4 +-
 2 files changed, 110 insertions(+), 3 deletions(-)
 create mode 100644 Mathlib/Data/Set/Dissipate.lean

diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean
new file mode 100644
index 00000000000000..d9a38cf1172ba3
--- /dev/null
+++ b/Mathlib/Data/Set/Dissipate.lean
@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2025 Peter Pfaffelhuber. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Peter Pfaffelhuber
+-/
+import Mathlib.Data.Set.Lattice
+
+/-!
+# Accumulate
+
+The function `Dissipate` takes a set `s` and returns `⋂ y ≤ x, s y`.
+-/
+
+
+variable {α β : Type*} {s : α → Set β}
+
+namespace Set
+
+/-- `Dissipate s` is the intersection of `s y` for `y ≤ x`. -/
+def Dissipate [LE α] (s : α → Set β) (x : α) : Set β :=
+  ⋂ y ≤ x, s y
+
+theorem dissipate_def [LE α] {x : α} : Dissipate s x = ⋂ y ≤ x, s y :=
+  rfl
+
+@[simp]
+theorem mem_dissipate [LE α] {x : α} {z : β} : z ∈ Dissipate s x ↔ ∀ y ≤ x, z ∈ s y := by
+  simp_rw [dissipate_def, mem_iInter₂]
+
+theorem dissipate_subset [Preorder α] {x y : α} (hy : y ≤ x): Dissipate s x ⊆ s y :=
+  biInter_subset_of_mem hy
+
+theorem dissipate_subset_iInter [Preorder α] (x : α) : ⋂ i, s i ⊆ Dissipate s x := by
+  simp [Dissipate]
+  exact fun x h ↦ iInter_subset_of_subset x fun ⦃a⦄ a ↦ a
+
+theorem antitone_dissipate [Preorder α] : Antitone (Dissipate s) :=
+  fun _ _ hab ↦ biInter_subset_biInter_left fun _ hz => le_trans hz hab
+
+@[gcongr]
+theorem dissipate_subset_dissipate [Preorder α] {x y} (h : y ≤ x) :
+    Dissipate s x ⊆ Dissipate s y :=
+  antitone_dissipate h
+
+#check antitone_dissipate
+
+example [Preorder α] (x : α) : x ≤ x := by exact Preorder.le_refl x
+
+@[simp]
+theorem biInter_dissipate [Preorder α] {s : α → Set β} {x : α} :
+    ⋂ y ≤ x, s y = ⋂ y ≤ x, ⋂ z ≤ y, s z := by
+  apply Set.Subset.antisymm
+  · sorry
+  · exact iInter₂_mono fun y _ => dissipate_subset (le_refl y)
+
+    have h := fun y hy ↦ antitone_dissipate hy
+    refine iInter₂_subset
+
+--    antitone_dissipate hy
+
+    sorry
+    simp only [subset_iInter_iff, Dissipate]
+    exact fun i hi z hz ↦ biInter_subset_of_mem <| le_trans hz hi
+  · apply iInter_mono
+    intro z y hy
+    simp only [mem_iInter, mem_dissipate] at *
+    exact fun h ↦ hy h z <| le_refl z
+
+@[simp]
+theorem biInter_dissipate [Preorder α] {s : α → Set β} {x : α} :
+    ⋂ y ≤ x, s y = ⋂ y ≤ x, ⋂ z ≤ y, s z := by
+  apply Set.Subset.antisymm
+  · simp only [subset_iInter_iff, Dissipate]
+    exact fun i hi z hz ↦ biInter_subset_of_mem <| le_trans hz hi
+  · apply iInter_mono
+    intro z y hy
+    simp only [mem_iInter, mem_dissipate] at *
+    exact fun h ↦ hy h z <| le_refl z
+
+
+theorem biInter_dissipate' [Preorder α] (x : α) : ⋃ y ≤ x, Accumulate s y = ⋃ y ≤ x, s y := by
+  apply Subset.antisymm
+  · exact iUnion₂_subset fun y hy => monotone_accumulate hy
+  · exact iUnion₂_mono fun y _ => subset_accumulate
+
+theorem iUnion_accumulate [Preorder α] : ⋃ x, Accumulate s x = ⋃ x, s x := by
+  apply Subset.antisymm
+  · simp only [subset_def, mem_iUnion, exists_imp, mem_accumulate]
+    intro z x x' ⟨_, hz⟩
+    exact ⟨x', hz⟩
+  · exact iUnion_mono fun i => subset_accumulate
+
+@[simp]
+lemma accumulate_bot [PartialOrder α] [OrderBot α] (s : α → Set β) : Accumulate s ⊥ = s ⊥ := by
+  simp [Set.accumulate_def]
+
+@[simp]
+lemma accumulate_zero_nat (s : ℕ → Set β) : Accumulate s 0 = s 0 := by
+  simp [accumulate_def]
+
+open Function in
+theorem disjoint_accumulate [Preorder α] (hs : Pairwise (Disjoint on s)) {i j : α} (hij : i < j) :
+    Disjoint (Accumulate s i) (s j) := by
+  apply disjoint_left.2 (fun x hx ↦ ?_)
+  simp only [Accumulate, mem_iUnion, exists_prop] at hx
+  rcases hx with ⟨k, hk, hx⟩
+  exact disjoint_left.1 (hs (hk.trans_lt hij).ne) hx
+
+end Set
diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 2b6251c95d39de..95ccca80427e27 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -170,9 +170,7 @@ lemma l10 (C : ℕ → Set α) (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2
       rw [hk, decumulate_succ, ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
   · have h3 (n : ℕ) : ∃ m, ⋂ i ≤ n, C i ⊇ C m := by
       induction n with
-      | zero =>
-        use 0
-        simp
+      | zero => use 0; simp
       | succ n hn =>
         obtain ⟨m, hm⟩ := hn
         rw [decumulate_succ]

From bbc424dbdecf781f895564ec0be526783b7fc173 Mon Sep 17 00:00:00 2001
From: pfaffelh <p.p@stochastik.uni-freiburg.de>
Date: Sun, 16 Feb 2025 00:21:22 +0100
Subject: [PATCH 08/53] added dissipate

---
 Mathlib/Data/Set/Dissipate.lean               | 106 +++++++++---------
 .../Topology/Compactness/CompactSystem.lean   |  31 ++---
 2 files changed, 64 insertions(+), 73 deletions(-)

diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean
index d9a38cf1172ba3..b340afa2d8c8b1 100644
--- a/Mathlib/Data/Set/Dissipate.lean
+++ b/Mathlib/Data/Set/Dissipate.lean
@@ -6,12 +6,11 @@ Authors: Peter Pfaffelhuber
 import Mathlib.Data.Set.Lattice
 
 /-!
-# Accumulate
+# Dissipate
 
 The function `Dissipate` takes a set `s` and returns `⋂ y ≤ x, s y`.
 -/
 
-
 variable {α β : Type*} {s : α → Set β}
 
 namespace Set
@@ -42,68 +41,71 @@ theorem dissipate_subset_dissipate [Preorder α] {x y} (h : y ≤ x) :
     Dissipate s x ⊆ Dissipate s y :=
   antitone_dissipate h
 
-#check antitone_dissipate
-
-example [Preorder α] (x : α) : x ≤ x := by exact Preorder.le_refl x
-
-@[simp]
-theorem biInter_dissipate [Preorder α] {s : α → Set β} {x : α} :
-    ⋂ y ≤ x, s y = ⋂ y ≤ x, ⋂ z ≤ y, s z := by
-  apply Set.Subset.antisymm
-  · sorry
-  · exact iInter₂_mono fun y _ => dissipate_subset (le_refl y)
-
-    have h := fun y hy ↦ antitone_dissipate hy
-    refine iInter₂_subset
-
---    antitone_dissipate hy
-
-    sorry
-    simp only [subset_iInter_iff, Dissipate]
-    exact fun i hi z hz ↦ biInter_subset_of_mem <| le_trans hz hi
-  · apply iInter_mono
-    intro z y hy
-    simp only [mem_iInter, mem_dissipate] at *
-    exact fun h ↦ hy h z <| le_refl z
-
 @[simp]
 theorem biInter_dissipate [Preorder α] {s : α → Set β} {x : α} :
     ⋂ y ≤ x, s y = ⋂ y ≤ x, ⋂ z ≤ y, s z := by
-  apply Set.Subset.antisymm
+  apply Subset.antisymm
   · simp only [subset_iInter_iff, Dissipate]
     exact fun i hi z hz ↦ biInter_subset_of_mem <| le_trans hz hi
-  · apply iInter_mono
-    intro z y hy
-    simp only [mem_iInter, mem_dissipate] at *
+  · apply iInter_mono fun z y hy ↦ ?_
+    simp only [mem_iInter] at *
     exact fun h ↦ hy h z <| le_refl z
 
+theorem iInter_dissipate [Preorder α] : ⋂ x, s x = ⋂ x, Dissipate s x := by
+  apply Subset.antisymm <;> simp [subset_def, mem_iInter, exists_imp, mem_dissipate]
+  · exact fun z h x' y hy ↦ h y
+  · exact fun z h x' ↦ h x' x' (le_refl x')
 
-theorem biInter_dissipate' [Preorder α] (x : α) : ⋃ y ≤ x, Accumulate s y = ⋃ y ≤ x, s y := by
-  apply Subset.antisymm
-  · exact iUnion₂_subset fun y hy => monotone_accumulate hy
-  · exact iUnion₂_mono fun y _ => subset_accumulate
+@[simp]
+lemma dissipate_bot [PartialOrder α] [OrderBot α] (s : α → Set β) : Dissipate s ⊥ = s ⊥ := by
+  simp [Set.dissipate_def]
 
-theorem iUnion_accumulate [Preorder α] : ⋃ x, Accumulate s x = ⋃ x, s x := by
-  apply Subset.antisymm
-  · simp only [subset_def, mem_iUnion, exists_imp, mem_accumulate]
-    intro z x x' ⟨_, hz⟩
-    exact ⟨x', hz⟩
-  · exact iUnion_mono fun i => subset_accumulate
+open Nat
 
 @[simp]
-lemma accumulate_bot [PartialOrder α] [OrderBot α] (s : α → Set β) : Accumulate s ⊥ = s ⊥ := by
-  simp [Set.accumulate_def]
+theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) :
+    Dissipate s (n + 1) = Dissipate s n ∩ s (n + 1) := by
+  ext x
+  refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
+  · simp only [mem_inter_iff, mem_iInter, Dissipate] at *
+    exact ⟨fun i hi ↦ hx i <| le_trans hi <|
+      le_add_right n 1, hx (n + 1) <| le_refl (n + 1)⟩
+  · simp only [Dissipate, mem_inter_iff, mem_iInter] at *
+    intro i hi
+    by_cases h : i ≤ n
+    · exact hx.1 i h
+    · simp only [not_le] at h
+      exact le_antisymm hi h ▸ hx.2
 
 @[simp]
-lemma accumulate_zero_nat (s : ℕ → Set β) : Accumulate s 0 = s 0 := by
-  simp [accumulate_def]
-
-open Function in
-theorem disjoint_accumulate [Preorder α] (hs : Pairwise (Disjoint on s)) {i j : α} (hij : i < j) :
-    Disjoint (Accumulate s i) (s j) := by
-  apply disjoint_left.2 (fun x hx ↦ ?_)
-  simp only [Accumulate, mem_iUnion, exists_prop] at hx
-  rcases hx with ⟨k, hk, hx⟩
-  exact disjoint_left.1 (hs (hk.trans_lt hij).ne) hx
+lemma dissipate_zero (s : ℕ → Set β) : Dissipate s 0 = s 0 := by
+  simp [dissipate_def]
+
+lemma subset_of_directed {C : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C)
+    (n : ℕ) : ∃ m, ⋂ i ≤ n, C i ⊇ C m := by
+  induction n with
+  | zero => use 0; simp
+  | succ n hn =>
+    obtain ⟨m, hm⟩ := hn
+    simp_rw [← dissipate_def, dissipate_succ]
+    obtain ⟨k, hk⟩ := hd m (n+1)
+    simp at hk
+    use k
+    simp only [subset_inter_iff]
+    exact ⟨le_trans hk.1 hm, hk.2⟩
+
+lemma empty_of_directed {C : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) :
+      (∃ n, C n = ∅) ↔ (∃ n, Dissipate C n = ∅) := by
+  refine ⟨fun ⟨n, hn⟩ ↦ ⟨n, ?_⟩, ?_⟩
+  · by_cases hn' : n = 0
+    · rw [hn']
+      exact Eq.trans (dissipate_zero C) (hn' ▸ hn)
+    · obtain ⟨k, hk⟩ := exists_eq_succ_of_ne_zero hn'
+      rw [hk, dissipate_succ, ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
+  · rw [← not_imp_not]
+    push_neg
+    intro h n
+    obtain ⟨m, hm⟩ := subset_of_directed hd n
+    exact Set.Nonempty.mono hm (h m)
 
 end Set
diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 95ccca80427e27..f75075a09431cd 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -33,20 +33,14 @@ def IsCompactSystem' (p : Set α → Prop) : Prop :=
   ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ (n : ℕ), (⋂ i ≤ n, C i).Nonempty) → (⋂ i, C i).Nonempty
 
 theorem IsCompactSystem_iff_IsCompactSystem' (p : Set α → Prop) :
-    IsCompactSystem p ↔ IsCompactSystem' p := by
-  refine ⟨fun h C hC hn ↦ ?_, fun h C hC ↦ ?_⟩
-  · have h2 := h C hC
-    rw [← not_imp_not] at h2
-    push_neg at h2
-    simp_rw [Set.nonempty_iff_ne_empty] at *
+    IsCompactSystem p ↔ (  ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ (n : ℕ),
+      (⋂ i ≤ n, C i).Nonempty) → (⋂ i, C i).Nonempty) := by
+  refine ⟨fun h C hC hn ↦ ?_, fun h C hC ↦ ?_⟩ <;> have h2 := not_imp_not.mpr <| h C hC
+  · push_neg at h2
     exact h2 hn
-  · have h2 := h C hC
-    rw [← not_imp_not] at h2
-    push_neg at h2
+  · push_neg at h2
     exact h2
 
-example (i n : ℕ) : i < n+1 ↔ i ≤ n := by exact Nat.lt_add_one_iff
-
 lemma l1 (s : Finset ℕ) (hs : s.Nonempty) : s ⊆ Finset.range (s.max' hs + 1) := by
   intro i hi
   rw [Finset.mem_range, Nat.lt_add_one_iff]
@@ -249,9 +243,9 @@ lemma l5 (p : α → Prop) (s : α) : p s ↔ (s ∈ ⋃ (i : α) (_ : p i), {i}
     simp only [mem_singleton_iff] at h
     exact h ▸ hi
 
-lemma l6 (p q : α → Prop) (s : α) : (p s ∧ q s) ↔ (s ∈ ⋃ (i : α) (_ : p i) (_ : q i), {i}) := by
-  rw [Set.mem_iUnion₂]
-  simp_rw [mem_iUnion]
+@[simp]
+lemma l6 {p q : α → Prop} {s : α} : (p s ∧ q s) ↔ (s ∈ ⋃ (i : α) (_ : p i) (_ : q i), {i}) := by
+  simp_rw [Set.mem_iUnion₂, mem_iUnion]
   refine ⟨fun h ↦ ?_, fun h ↦ ?_ ⟩
   · use s, h.1, h.2
     simp only [mem_singleton_iff]
@@ -259,9 +253,6 @@ lemma l6 (p q : α → Prop) (s : α) : (p s ∧ q s) ↔ (s ∈ ⋃ (i : α) (_
     simp only [mem_singleton_iff] at h2
     exact h2 ▸ ⟨hi, h1⟩
 
-lemma l7 (p : α → Prop) (s : α) : (s ∈ ⋃ (i : α) (_ : p i), {i}) ↔ (⋃ (i : α) (_ : p i), {i}) s:= by
-  rfl
-
 variable {α : Type*} [TopologicalSpace α]
 
 example (x y : Set α) (hx : IsClosed x) (hy : IsClosed y) : IsClosed (x ∩ y) := by
@@ -272,13 +263,11 @@ theorem IsCompact.isCompactSystem {α : Type*} [Inhabited α] [TopologicalSpace
     IsCompactSystem (⋃ (s : Set α) (_ : IsCompact s) (_ : IsClosed s), {s}) := by
   have h : IsPiSystem' (⋃ (s : Set α) (_ : IsCompact s) (_ : IsClosed s), {s}) := by
     intro x hx y hy
-    rw [← (l6 IsCompact IsClosed)] at *
+    rw [← l6] at *
     exact ⟨IsCompact.inter_left hy.1 hx.2, IsClosed.inter hx.2 hy.2 ⟩
   rw [IsCompactSystem.iff_mono' h]
   intro C hC h1 hn
-  have h1' (i : ℕ) : IsCompact (C i) ∧ IsClosed (C i):= by
-    rw [(l6 IsCompact IsClosed (C i))]
-    exact h1 i
+  have h1' (i : ℕ) : IsCompact (C i) ∧ IsClosed (C i):= l6.mpr <| h1 i
   exact IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed C hC hn
     (fun i ↦ (h1' i).1) (fun i ↦ (h1' i).2)
 

From e2840e725b2e3468a020975754cab93479887f44 Mon Sep 17 00:00:00 2001
From: pfaffelh <p.p@stochastik.uni-freiburg.de>
Date: Sun, 16 Feb 2025 20:26:03 +0100
Subject: [PATCH 09/53] small update

---
 .../Topology/Compactness/CompactSystem.lean   | 22 ++++---------------
 1 file changed, 4 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index f75075a09431cd..435dc91ad92358 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -131,7 +131,7 @@ theorem iInter_decumulate (s : ℕ → Set α) : ⋂ x, ⋂ y ≤ x, s y = ⋂ y
 
 def IsPiSystem' (C : Set (Set α)) := ∀ s ∈ C, ∀ t ∈ C, s ∩ t ∈ C
 
-lemma prime (C : Set (Set α)) (hC : ∅ ∈ C) : (IsPiSystem C) ↔ (IsPiSystem' C) := by
+lemma prime (C : Set (Set α)) (hC : ∅ ∈ C) : (IsPiSystem C) ↔ (∀ s ∈ C, ∀ t ∈ C, s ∩ t ∈ C) := by
   refine ⟨fun h s hs t ht ↦ ?_, fun h s hs t ht _ ↦ h s hs t ht⟩
   by_cases h' : (s ∩ t).Nonempty
   · exact h s hs t ht h'
@@ -208,9 +208,6 @@ theorem IsCompactSystem.iff_mono [Inhabited α] (hpi : IsPiSystem' p) : (IsCompa
     rcases h5 with ⟨n, hn⟩
     use n
 
-example (P Q : Prop) : (P → Q) ↔ (¬ Q → ¬ P) := by exact Iff.symm not_imp_not
-
-
 theorem IsCompactSystem.iff_mono' [Inhabited α] (hpi : IsPiSystem' p) : (IsCompactSystem p) ↔
   ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
     (∀ (n : ℕ), (C n).Nonempty) →
@@ -245,21 +242,12 @@ lemma l5 (p : α → Prop) (s : α) : p s ↔ (s ∈ ⋃ (i : α) (_ : p i), {i}
 
 @[simp]
 lemma l6 {p q : α → Prop} {s : α} : (p s ∧ q s) ↔ (s ∈ ⋃ (i : α) (_ : p i) (_ : q i), {i}) := by
-  simp_rw [Set.mem_iUnion₂, mem_iUnion]
-  refine ⟨fun h ↦ ?_, fun h ↦ ?_ ⟩
-  · use s, h.1, h.2
-    simp only [mem_singleton_iff]
-  · obtain ⟨i, hi, h1, h2⟩ := h
-    simp only [mem_singleton_iff] at h2
-    exact h2 ▸ ⟨hi, h1⟩
+  simp_rw [Set.mem_iUnion₂, mem_iUnion, mem_singleton_iff]
+  refine ⟨fun h ↦ ⟨s, h.1, h.2, rfl⟩, fun ⟨i, hi, h1, h2⟩ ↦ h2 ▸ ⟨hi, h1⟩⟩
 
 variable {α : Type*} [TopologicalSpace α]
 
-example (x y : Set α) (hx : IsClosed x) (hy : IsClosed y) : IsClosed (x ∩ y) := by
-  exact IsClosed.inter hx hy
-
-
-theorem IsCompact.isCompactSystem {α : Type*} [Inhabited α] [TopologicalSpace α] :
+theorem IsClosedCompact.isCompactSystem {α : Type*} [Inhabited α] [TopologicalSpace α] :
     IsCompactSystem (⋃ (s : Set α) (_ : IsCompact s) (_ : IsClosed s), {s}) := by
   have h : IsPiSystem' (⋃ (s : Set α) (_ : IsCompact s) (_ : IsClosed s), {s}) := by
     intro x hx y hy
@@ -271,8 +259,6 @@ theorem IsCompact.isCompactSystem {α : Type*} [Inhabited α] [TopologicalSpace
   exact IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed C hC hn
     (fun i ↦ (h1' i).1) (fun i ↦ (h1' i).2)
 
-
-
 end Compact
 
 /--

From 960f09c02a9a18cd5ca0f5df04467155f3a1472e Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@pc.fritz.box>
Date: Sun, 16 Feb 2025 23:41:44 +0100
Subject: [PATCH 10/53] cleaning

---
 Mathlib/Data/Set/Dissipate.lean               |  30 ++-
 .../Topology/Compactness/CompactSystem.lean   | 203 +++---------------
 2 files changed, 58 insertions(+), 175 deletions(-)

diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean
index b340afa2d8c8b1..a1503199c3660d 100644
--- a/Mathlib/Data/Set/Dissipate.lean
+++ b/Mathlib/Data/Set/Dissipate.lean
@@ -19,6 +19,7 @@ namespace Set
 def Dissipate [LE α] (s : α → Set β) (x : α) : Set β :=
   ⋂ y ≤ x, s y
 
+@[simp]
 theorem dissipate_def [LE α] {x : α} : Dissipate s x = ⋂ y ≤ x, s y :=
   rfl
 
@@ -52,7 +53,7 @@ theorem biInter_dissipate [Preorder α] {s : α → Set β} {x : α} :
     exact fun h ↦ hy h z <| le_refl z
 
 theorem iInter_dissipate [Preorder α] : ⋂ x, s x = ⋂ x, Dissipate s x := by
-  apply Subset.antisymm <;> simp [subset_def, mem_iInter, exists_imp, mem_dissipate]
+  apply Subset.antisymm <;> simp_rw [subset_def, mem_iInter, mem_dissipate]
   · exact fun z h x' y hy ↦ h y
   · exact fun z h x' ↦ h x' x' (le_refl x')
 
@@ -81,8 +82,8 @@ theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) :
 lemma dissipate_zero (s : ℕ → Set β) : Dissipate s 0 = s 0 := by
   simp [dissipate_def]
 
-lemma subset_of_directed {C : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C)
-    (n : ℕ) : ∃ m, ⋂ i ≤ n, C i ⊇ C m := by
+lemma subset_of_directed {s : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) s)
+    (n : ℕ) : ∃ m, ⋂ i ≤ n, s i ⊇ s m := by
   induction n with
   | zero => use 0; simp
   | succ n hn =>
@@ -94,12 +95,12 @@ lemma subset_of_directed {C : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set 
     simp only [subset_inter_iff]
     exact ⟨le_trans hk.1 hm, hk.2⟩
 
-lemma empty_of_directed {C : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) :
-      (∃ n, C n = ∅) ↔ (∃ n, Dissipate C n = ∅) := by
+lemma empty_of_directed {s : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) s) :
+      (∃ n, s n = ∅) ↔ (∃ n, Dissipate s n = ∅) := by
   refine ⟨fun ⟨n, hn⟩ ↦ ⟨n, ?_⟩, ?_⟩
   · by_cases hn' : n = 0
     · rw [hn']
-      exact Eq.trans (dissipate_zero C) (hn' ▸ hn)
+      exact Eq.trans (dissipate_zero s) (hn' ▸ hn)
     · obtain ⟨k, hk⟩ := exists_eq_succ_of_ne_zero hn'
       rw [hk, dissipate_succ, ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
   · rw [← not_imp_not]
@@ -108,4 +109,21 @@ lemma empty_of_directed {C : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α
     obtain ⟨m, hm⟩ := subset_of_directed hd n
     exact Set.Nonempty.mono hm (h m)
 
+lemma dissipate_directed {s : ℕ → Set α} :
+    Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) fun n ↦ Dissipate s n := by
+  refine directed_of_isDirected_le ?_
+  intro i j hij
+  exact dissipate_subset_dissipate hij
+
+lemma dissipate_of_piSystem {s : ℕ → Set α} {p : Set α → Prop}
+    (hp : ∀ (s t : Set α), p s → p t → p (s ∩ t)) (h : ∀ n, p (s n)) (n : ℕ) :
+      p (Dissipate s n) := by
+  induction n with
+  | zero =>
+    simp only [dissipate_def, le_zero_eq, iInter_iInter_eq_left]
+    exact h 0
+  | succ n hn =>
+    rw [dissipate_succ]
+    exact hp (Dissipate s n) (s (n+1)) hn (h (n+1))
+
 end Set
diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 435dc91ad92358..bc0d4f3e968b98 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Peter Pfaffelhuber
 -/
+import Mathlib.Data.Set.Dissipate
 import Mathlib.Topology.Compactness.Compact
 import Mathlib.MeasureTheory.PiSystem
 
@@ -29,11 +30,8 @@ lemma IsCompactSystem.iInter_eq_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C
     ⋂ i ≤ hp.max_of_empty hC hC_empty, C i = ∅ :=
   (hp C hC hC_empty).choose_spec
 
-def IsCompactSystem' (p : Set α → Prop) : Prop :=
-  ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ (n : ℕ), (⋂ i ≤ n, C i).Nonempty) → (⋂ i, C i).Nonempty
-
-theorem IsCompactSystem_iff_IsCompactSystem' (p : Set α → Prop) :
-    IsCompactSystem p ↔ (  ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ (n : ℕ),
+theorem IsCompactSystem_iff_of_nempty (p : Set α → Prop) :
+    IsCompactSystem p ↔ (∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ (n : ℕ),
       (⋂ i ≤ n, C i).Nonempty) → (⋂ i, C i).Nonempty) := by
   refine ⟨fun h C hC hn ↦ ?_, fun h C hC ↦ ?_⟩ <;> have h2 := not_imp_not.mpr <| h C hC
   · push_neg at h2
@@ -41,96 +39,6 @@ theorem IsCompactSystem_iff_IsCompactSystem' (p : Set α → Prop) :
   · push_neg at h2
     exact h2
 
-lemma l1 (s : Finset ℕ) (hs : s.Nonempty) : s ⊆ Finset.range (s.max' hs + 1) := by
-  intro i hi
-  rw [Finset.mem_range, Nat.lt_add_one_iff]
-  exact s.le_max' i hi
-
-example (s : Finset ℕ) (hs : s.Nonempty) (i : ℕ) (hi : i ∈ s) : i ≤ s.max' hs := by
-  exact Finset.le_max' s i hi
-
-example (i n : ℕ) : i ∈ Finset.range (n + 1) ↔ i ≤ n := by exact Finset.mem_range_succ_iff
-
-example (n : ℕ) : { i // i < n+1} = {i // i ≤ n} := by
-    simp_rw [Nat.lt_add_one_iff]
-
-example (i n : ℕ) : i < n+1 ↔ i ≤ n := by exact Nat.lt_add_one_iff
-
-example (C : ℕ → Set α) (n : ℕ) : ⋂ i < n+1, C i = ⋂ i ≤ n, C i :=
-  by simp_rw [Nat.lt_add_one_iff]
-
-example (n : ℕ) : (Finset.range (n + 1)).Nonempty := by exact Finset.nonempty_range_succ
-
-@[simp]
-lemma iInter_empty_iff [Inhabited α] {C : ℕ → Set α} : (∃ n : ℕ, ⋂ i ≤ n, C i = ∅) ↔
-    (∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅) := by
-  refine ⟨fun ⟨n, hn⟩ ↦ ?_, fun ⟨s, hs⟩ ↦ ?_⟩
-  · use (Finset.range (n + 1))
-    simp_rw [Finset.mem_range_succ_iff]
-    exact hn
-  · have h2 : s.Nonempty := by
-      rw [s.nonempty_iff_ne_empty]
-      intro h
-      rw [h] at hs
-      simp only [Finset.not_mem_empty, iInter_of_empty, iInter_univ, Set.univ_eq_empty_iff,
-        not_isEmpty_of_nonempty] at hs
-    use (s.max' h2)
-    have h : ⋂ i, ⋂ (_ : i ≤ s.max' h2), C i ⊆ ⋂ i ∈ s, C i := by
-      simp_rw [← Finset.mem_range_succ_iff]
-      exact biInter_mono (l1 s h2) (fun _ _ ⦃a_1⦄ a ↦ a)
-    exact subset_empty_iff.mp <| le_trans h hs.le
-
-
-
-
-theorem IsCompactSystem.iff_le [Inhabited α] : (IsCompactSystem p) ↔
-    (∀ C : ℕ → Set α, (∀ i, p (C i)) → ⋂ i, C i = ∅ → ∃ (s : Finset ℕ), ⋂ i ∈ s, C i = ∅) := by
-  refine ⟨fun h C hp he ↦ ?_, fun h C hp he ↦ ?_ ⟩
-  · apply iInter_empty_iff.mp <| h C hp he
-  · apply iInter_empty_iff.mpr <| h C hp he
-
-
-
-
-theorem biInter_decumulate (s : ℕ → Set α) (n : ℕ):
-    ⋂ x ≤ n, ⋂ y ≤ x, s y = ⋂ y ≤ n, s y := by
-  apply Set.Subset.antisymm
-  · apply iInter_mono
-    intro z x hx
-    simp at hx
-    simp only [mem_iInter]
-    exact fun h ↦ hx h z <| Nat.le_refl z
-  · simp only [subset_iInter_iff]
-    intro i hi x hx
-    refine biInter_subset_of_mem ?_
-    simp only [le_eq]
-    exact le_trans hx hi
-
-theorem decumulate_succ (s : ℕ → Set α) (n : ℕ) :
-    ⋂ i ≤ n + 1, s i = (⋂ i ≤ n, s i) ∩ s (n + 1) := by
-  ext x
-  refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
-  · simp only [mem_inter_iff, mem_iInter] at *
-    exact ⟨fun i hi ↦ hx i <| le_trans hi <| le_add_right n 1, hx (n + 1) <| Nat.le_refl (n + 1)⟩
-  · simp only [mem_inter_iff, mem_iInter] at *
-    intro i hi
-    by_cases h : i ≤ n
-    · exact hx.1 i h
-    · simp only [not_le] at h
-      exact Nat.le_antisymm hi h ▸ hx.2
-
-theorem iInter_decumulate (s : ℕ → Set α) : ⋂ x, ⋂ y ≤ x, s y = ⋂ y, s y := by
-  apply Set.Subset.antisymm
-  · apply iInter_mono
-    intro z x hx
-    simp at hx
-    apply hx z <| Nat.le_refl z
-  · simp only [subset_iInter_iff]
-    intro i x hx
-    exact iInter_subset_of_subset x fun ⦃a⦄ a ↦ a
-
-def IsPiSystem' (C : Set (Set α)) := ∀ s ∈ C, ∀ t ∈ C, s ∩ t ∈ C
-
 lemma prime (C : Set (Set α)) (hC : ∅ ∈ C) : (IsPiSystem C) ↔ (∀ s ∈ C, ∀ t ∈ C, s ∩ t ∈ C) := by
   refine ⟨fun h s hs t ht ↦ ?_, fun h s hs t ht _ ↦ h s hs t ht⟩
   by_cases h' : (s ∩ t).Nonempty
@@ -138,19 +46,6 @@ lemma prime (C : Set (Set α)) (hC : ∅ ∈ C) : (IsPiSystem C) ↔ (∀ s ∈
   · push_neg at h'
     exact h' ▸ hC
 
-example (C D : ℕ → Set α) (n : ℕ) (hCD : C = D) : ⋂ i ≤ n, C i = ⋂ i ≤ n, D i := by
-  exact iInter₂_congr fun i j ↦ congrFun hCD i
-
-lemma l2 (C : Set (Set α)) (hC : IsPiSystem' C) (s : ℕ → Set α) (hs : ∀ n, s n ∈ C) (n : ℕ) :
-    ⋂ i ≤ n, s i ∈ C :=  by
-  induction n with
-  | zero =>
-    simp only [le_zero_eq, iInter_iInter_eq_left]
-    exact hs 0
-  | succ n hn =>
-    rw [decumulate_succ s n]
-    exact hC (⋂ i, ⋂ (_ : i ≤ n), s i) hn (s (n + 1)) (hs (n + 1))
-
 lemma l10 (C : ℕ → Set α) (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) :
       (∃ n, C n = ∅) ↔ (∃ n, ⋂ i ≤ n, C i = ∅) := by
   refine ⟨fun h ↦ ?_, ?_⟩
@@ -161,13 +56,14 @@ lemma l10 (C : ℕ → Set α) (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2
       simp only [le_zero_eq, iInter_iInter_eq_left]
       exact hn' ▸ hn
     · obtain ⟨k, hk⟩ := exists_eq_succ_of_ne_zero hn'
-      rw [hk, decumulate_succ, ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
+      simp_rw [hk, succ_eq_add_one, ← dissipate_def, dissipate_succ,
+        ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
   · have h3 (n : ℕ) : ∃ m, ⋂ i ≤ n, C i ⊇ C m := by
       induction n with
       | zero => use 0; simp
       | succ n hn =>
         obtain ⟨m, hm⟩ := hn
-        rw [decumulate_succ]
+        simp_rw [← dissipate_def, dissipate_succ]
         obtain ⟨k, hk⟩ := hd m (n+1)
         simp at hk
         use k
@@ -181,48 +77,24 @@ lemma l10 (C : ℕ → Set α) (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2
     obtain ⟨m, hm⟩ := h3 n
     exact Set.Nonempty.mono hm (h m)
 
-theorem IsCompactSystem.iff_mono [Inhabited α] (hpi : IsPiSystem' p) : (IsCompactSystem p) ↔
+theorem IsCompactSystem.iff_mono [Inhabited α] (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
+    (IsCompactSystem p) ↔
     (∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
       ⋂ i, C i = ∅ → ∃ (n : ℕ), C n = ∅) := by
   refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩
   · rw [l10 C hdi]
     exact h C hi
-  · let D := fun n ↦ ⋂ i ≤ n, C i
-    have h' := h C
-    have h8 (n : ℕ) : ⋂ i ≤ n, D i = ⋂ i ≤ n, C i := biInter_decumulate C n
-    have h1' : ⋂ i, D i = ⋂ i, C i := by exact biInter_le_eq_iInter
-    have h9 : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) D := by
-      refine directed_of_isDirected_le ?_
-      intro i j hij
-      simp [D]
-      intro k hk
-      refine biInter_subset_of_mem ?_
-      exact le_trans hk hij
-    have h3 (i : ℕ) : p (D i) := by
-      simp [D, hpi]
-      obtain h4 := l2 {s : Set α | p s} hpi C
-      obtain h5 := h4 h1 i
-      exact h5
-    obtain h5 := h D h9 h3 (h1' ▸  h2)
-    obtain h6 := h D h9
-    rcases h5 with ⟨n, hn⟩
-    use n
+  · rw [← biInter_le_eq_iInter] at h2
+    exact h (Dissipate C) dissipate_directed (dissipate_of_piSystem hpi h1) h2
 
-theorem IsCompactSystem.iff_mono' [Inhabited α] (hpi : IsPiSystem' p) : (IsCompactSystem p) ↔
-  ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
-    (∀ (n : ℕ), (C n).Nonempty) →
-      (⋂ i, C i).Nonempty  := by
+theorem IsCompactSystem.iff_mono' [Inhabited α] (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
+    (IsCompactSystem p) ↔
+    ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
+    (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty  := by
   rw [IsCompactSystem.iff_mono hpi]
-  refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 ↦ ?_⟩
-  · rw [← not_imp_not]
-    push_neg
-    exact h1 C h3 h4
-  · intro s
-    rw [← not_imp_not]
-    push_neg
-    exact h1 C h3 s
-
-
+  refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 s ↦ ?_⟩ <;> rw [← not_imp_not] <;> push_neg
+  · exact h1 C h3 h4
+  · exact h1 C h3 s
 
 end definition
 
@@ -230,34 +102,27 @@ section Compact
 
 variable {α : Type*}
 
-@[simp]
-lemma l5 (p : α → Prop) (s : α) : p s ↔ (s ∈ ⋃ (i : α) (_ : p i), {i}) := by
-  rw [Set.mem_iUnion₂]
-  refine ⟨fun h ↦ ?_, fun h ↦ ?_ ⟩
-  · use s, h
-    simp only [mem_singleton_iff]
-  · obtain ⟨i, hi, h⟩ := h
-    simp only [mem_singleton_iff] at h
-    exact h ▸ hi
-
-@[simp]
-lemma l6 {p q : α → Prop} {s : α} : (p s ∧ q s) ↔ (s ∈ ⋃ (i : α) (_ : p i) (_ : q i), {i}) := by
-  simp_rw [Set.mem_iUnion₂, mem_iUnion, mem_singleton_iff]
-  refine ⟨fun h ↦ ⟨s, h.1, h.2, rfl⟩, fun ⟨i, hi, h1, h2⟩ ↦ h2 ▸ ⟨hi, h1⟩⟩
-
 variable {α : Type*} [TopologicalSpace α]
 
+example (s t : Set α) (hs : IsClosed s) (ht : IsClosed t) : IsClosed (s ∩ t) := by
+  exact IsClosed.inter hs ht
+
+example : IsCompact (∅ : Set α) := by exact isCompact_empty
+
 theorem IsClosedCompact.isCompactSystem {α : Type*} [Inhabited α] [TopologicalSpace α] :
-    IsCompactSystem (⋃ (s : Set α) (_ : IsCompact s) (_ : IsClosed s), {s}) := by
-  have h : IsPiSystem' (⋃ (s : Set α) (_ : IsCompact s) (_ : IsClosed s), {s}) := by
-    intro x hx y hy
-    rw [← l6] at *
+    IsCompactSystem (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by
+  have h : IsPiSystem ({ s : Set α | IsCompact s ∧ IsClosed s}) := by
+    intro x hx y hy _
     exact ⟨IsCompact.inter_left hy.1 hx.2, IsClosed.inter hx.2 hy.2 ⟩
-  rw [IsCompactSystem.iff_mono' h]
-  intro C hC h1 hn
-  have h1' (i : ℕ) : IsCompact (C i) ∧ IsClosed (C i):= l6.mpr <| h1 i
-  exact IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed C hC hn
-    (fun i ↦ (h1' i).1) (fun i ↦ (h1' i).2)
+  have h1 : ∅ ∈ {s : Set α| IsCompact s ∧ IsClosed s} := by
+    exact ⟨isCompact_empty, isClosed_empty⟩
+  have h2 : ∀ (s t : Set α), IsCompact s ∧ IsClosed s →
+      IsCompact t ∧ IsClosed t → IsCompact (s ∩ t) ∧ IsClosed (s ∩ t) :=
+    fun s t h1 h2 ↦ ⟨IsCompact.inter_right h1.1 h2.2, IsClosed.inter h1.2 h2.2⟩
+  rw [prime _ h1] at h
+  rw [IsCompactSystem.iff_mono' h2]
+  exact fun s hs h1 h2 ↦ IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed s hs h2
+    (fun i ↦ (h1 i).1) (fun i ↦ (h1 i).2)
 
 end Compact
 

From ee70c17ffd328a7af950a09eb08ac1b6f96ea512 Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@pc.fritz.box>
Date: Mon, 17 Feb 2025 00:05:57 +0100
Subject: [PATCH 11/53] cleaning2

---
 Mathlib/Data/Set/Dissipate.lean               | 27 +++++++++++++++
 .../Topology/Compactness/CompactSystem.lean   | 33 +------------------
 2 files changed, 28 insertions(+), 32 deletions(-)

diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean
index a1503199c3660d..3713fa64e94e15 100644
--- a/Mathlib/Data/Set/Dissipate.lean
+++ b/Mathlib/Data/Set/Dissipate.lean
@@ -115,6 +115,33 @@ lemma dissipate_directed {s : ℕ → Set α} :
   intro i j hij
   exact dissipate_subset_dissipate hij
 
+lemma mem_subset_dissipate_of_directed (C : ℕ → Set α)
+    (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) (n : ℕ) : ∃ m, Dissipate C n ⊇ C m := by
+  induction n with
+  | zero => use 0; simp
+  | succ n hn =>
+    obtain ⟨m, hm⟩ := hn
+    obtain ⟨k, hk⟩ := hd m (n+1)
+    simp_rw [dissipate_succ]
+    simp at hk
+    exact ⟨k, Set.subset_inter_iff.mpr <| ⟨le_trans hk.1 hm, hk.2⟩⟩
+
+lemma dissipate_exists_empty_iff_of_directed (C : ℕ → Set α)
+    (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) :
+      (∃ n, C n = ∅) ↔ (∃ n, Dissipate C n = ∅) := by
+  refine ⟨fun ⟨n, hn⟩ ↦ ⟨n, ?_⟩ , ?_⟩
+  · by_cases hn' : n = 0
+    · rw [hn', dissipate_zero]
+      exact hn' ▸ hn
+    · obtain ⟨k, hk⟩ := exists_eq_succ_of_ne_zero hn'
+      simp_rw [hk, succ_eq_add_one, dissipate_succ,
+        ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
+  · rw [← not_imp_not]
+    push_neg
+    intro h n
+    obtain ⟨m, hm⟩ := mem_subset_dissipate_of_directed C hd n
+    exact Set.Nonempty.mono hm (h m)
+
 lemma dissipate_of_piSystem {s : ℕ → Set α} {p : Set α → Prop}
     (hp : ∀ (s t : Set α), p s → p t → p (s ∩ t)) (h : ∀ n, p (s n)) (n : ℕ) :
       p (Dissipate s n) := by
diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index bc0d4f3e968b98..eb1ce7f8188391 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -46,43 +46,12 @@ lemma prime (C : Set (Set α)) (hC : ∅ ∈ C) : (IsPiSystem C) ↔ (∀ s ∈
   · push_neg at h'
     exact h' ▸ hC
 
-lemma l10 (C : ℕ → Set α) (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) :
-      (∃ n, C n = ∅) ↔ (∃ n, ⋂ i ≤ n, C i = ∅) := by
-  refine ⟨fun h ↦ ?_, ?_⟩
-  · obtain ⟨n, hn⟩ := h
-    use n
-    by_cases hn' : n = 0
-    · rw [hn']
-      simp only [le_zero_eq, iInter_iInter_eq_left]
-      exact hn' ▸ hn
-    · obtain ⟨k, hk⟩ := exists_eq_succ_of_ne_zero hn'
-      simp_rw [hk, succ_eq_add_one, ← dissipate_def, dissipate_succ,
-        ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
-  · have h3 (n : ℕ) : ∃ m, ⋂ i ≤ n, C i ⊇ C m := by
-      induction n with
-      | zero => use 0; simp
-      | succ n hn =>
-        obtain ⟨m, hm⟩ := hn
-        simp_rw [← dissipate_def, dissipate_succ]
-        obtain ⟨k, hk⟩ := hd m (n+1)
-        simp at hk
-        use k
-        simp only [Set.subset_inter_iff]
-        exact ⟨le_trans hk.1 hm, hk.2⟩
-    rw [← not_imp_not]
-    push_neg
-    intro h n
-    obtain h2 := hd n (n + 1)
-    simp at h2
-    obtain ⟨m, hm⟩ := h3 n
-    exact Set.Nonempty.mono hm (h m)
-
 theorem IsCompactSystem.iff_mono [Inhabited α] (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
     (IsCompactSystem p) ↔
     (∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
       ⋂ i, C i = ∅ → ∃ (n : ℕ), C n = ∅) := by
   refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩
-  · rw [l10 C hdi]
+  · rw [dissipate_exists_empty_iff_of_directed C hdi]
     exact h C hi
   · rw [← biInter_le_eq_iInter] at h2
     exact h (Dissipate C) dissipate_directed (dissipate_of_piSystem hpi h1) h2

From b8ab9fe58e842bb112d23bb085a766964d44d8f4 Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@pc.fritz.box>
Date: Mon, 17 Feb 2025 00:06:11 +0100
Subject: [PATCH 12/53] cleaning3

---
 Mathlib/Data/Set/Dissipate.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean
index 3713fa64e94e15..af81770e7fdf27 100644
--- a/Mathlib/Data/Set/Dissipate.lean
+++ b/Mathlib/Data/Set/Dissipate.lean
@@ -110,10 +110,8 @@ lemma empty_of_directed {s : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α
     exact Set.Nonempty.mono hm (h m)
 
 lemma dissipate_directed {s : ℕ → Set α} :
-    Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) fun n ↦ Dissipate s n := by
-  refine directed_of_isDirected_le ?_
-  intro i j hij
-  exact dissipate_subset_dissipate hij
+    Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) fun n ↦ Dissipate s n :=
+  directed_of_isDirected_le <| fun _ _ hij ↦ dissipate_subset_dissipate hij
 
 lemma mem_subset_dissipate_of_directed (C : ℕ → Set α)
     (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) (n : ℕ) : ∃ m, Dissipate C n ⊇ C m := by

From b0ae9b5b3bf15fb46c34b9b3a38012ae4181f4a5 Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Mon, 17 Feb 2025 08:55:01 +0100
Subject: [PATCH 13/53] added mono from diss

---
 Mathlib/Data/Set/Dissipate.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean
index af81770e7fdf27..fc3a270c68ac77 100644
--- a/Mathlib/Data/Set/Dissipate.lean
+++ b/Mathlib/Data/Set/Dissipate.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Peter Pfaffelhuber
 -/
 import Mathlib.Data.Set.Lattice
+import Mathlib.Order.Directed
 
 /-!
 # Dissipate
@@ -111,7 +112,7 @@ lemma empty_of_directed {s : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α
 
 lemma dissipate_directed {s : ℕ → Set α} :
     Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) fun n ↦ Dissipate s n :=
-  directed_of_isDirected_le <| fun _ _ hij ↦ dissipate_subset_dissipate hij
+     antitone_dissipate.directed_ge
 
 lemma mem_subset_dissipate_of_directed (C : ℕ → Set α)
     (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) (n : ℕ) : ∃ m, Dissipate C n ⊇ C m := by

From 3dc1996a67ee2a548eacec2665bab502bc68d72e Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Fri, 21 Feb 2025 09:21:09 +0100
Subject: [PATCH 14/53] diss

---
 Mathlib/Data/Set/Dissipate.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean
index fc3a270c68ac77..403c6a14de6fd2 100644
--- a/Mathlib/Data/Set/Dissipate.lean
+++ b/Mathlib/Data/Set/Dissipate.lean
@@ -21,8 +21,7 @@ def Dissipate [LE α] (s : α → Set β) (x : α) : Set β :=
   ⋂ y ≤ x, s y
 
 @[simp]
-theorem dissipate_def [LE α] {x : α} : Dissipate s x = ⋂ y ≤ x, s y :=
-  rfl
+theorem dissipate_def [LE α] {x : α} : Dissipate s x = ⋂ y ≤ x, s y := rfl
 
 @[simp]
 theorem mem_dissipate [LE α] {x : α} {z : β} : z ∈ Dissipate s x ↔ ∀ y ≤ x, z ∈ s y := by
@@ -32,7 +31,7 @@ theorem dissipate_subset [Preorder α] {x y : α} (hy : y ≤ x): Dissipate s x
   biInter_subset_of_mem hy
 
 theorem dissipate_subset_iInter [Preorder α] (x : α) : ⋂ i, s i ⊆ Dissipate s x := by
-  simp [Dissipate]
+  simp only [Dissipate, subset_iInter_iff]
   exact fun x h ↦ iInter_subset_of_subset x fun ⦃a⦄ a ↦ a
 
 theorem antitone_dissipate [Preorder α] : Antitone (Dissipate s) :=
@@ -111,7 +110,7 @@ lemma empty_of_directed {s : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α
     exact Set.Nonempty.mono hm (h m)
 
 lemma dissipate_directed {s : ℕ → Set α} :
-    Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) fun n ↦ Dissipate s n :=
+    Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) (Dissipate s) :=
      antitone_dissipate.directed_ge
 
 lemma mem_subset_dissipate_of_directed (C : ℕ → Set α)
@@ -141,6 +140,8 @@ lemma dissipate_exists_empty_iff_of_directed (C : ℕ → Set α)
     obtain ⟨m, hm⟩ := mem_subset_dissipate_of_directed C hd n
     exact Set.Nonempty.mono hm (h m)
 
+/-- For a ∩-stable attribute `p` on `Set α` and a sequence of sets `s` with this attribute,
+`p ⋂ i ≤ n, s n` holds. -/
 lemma dissipate_of_piSystem {s : ℕ → Set α} {p : Set α → Prop}
     (hp : ∀ (s t : Set α), p s → p t → p (s ∩ t)) (h : ∀ n, p (s n)) (n : ℕ) :
       p (Dissipate s n) := by

From 3e0004c1fb3c7779ec8055fc2d30bc3ca7dc5783 Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Fri, 21 Feb 2025 11:01:50 +0100
Subject: [PATCH 15/53] final?

---
 Mathlib/MeasureTheory/PiSystem.lean           |   8 +
 .../Topology/Compactness/CompactSystem.lean   | 324 +++---------------
 2 files changed, 51 insertions(+), 281 deletions(-)

diff --git a/Mathlib/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean
index 4e01f2680951a7..871fc68388d14b 100644
--- a/Mathlib/MeasureTheory/PiSystem.lean
+++ b/Mathlib/MeasureTheory/PiSystem.lean
@@ -97,6 +97,14 @@ theorem IsPiSystem.insert_univ {S : Set (Set α)} (h_pi : IsPiSystem S) :
     · simp [hs, ht]
     · exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)
 
+lemma IsPiSystem.iff_of_empty_mem (S : Set (Set α)) (hS : ∅ ∈ S) :
+    (IsPiSystem S) ↔ (∀ s ∈ S, ∀ t ∈ S, s ∩ t ∈ S) := by
+  refine ⟨fun h s hs t ht ↦ ?_, fun h s hs t ht _ ↦ h s hs t ht⟩
+  by_cases h' : (s ∩ t).Nonempty
+  · exact h s hs t ht h'
+  · push_neg at h'
+    exact h' ▸ hS
+
 theorem IsPiSystem.comap {α β} {S : Set (Set β)} (h_pi : IsPiSystem S) (f : α → β) :
     IsPiSystem { s : Set α | ∃ t ∈ S, f ⁻¹' t = s } := by
   rintro _ ⟨s, hs_mem, rfl⟩ _ ⟨t, ht_mem, rfl⟩ hst
diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index eb1ce7f8188391..bae79df4393bf8 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -4,9 +4,27 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Peter Pfaffelhuber
 -/
 import Mathlib.Data.Set.Dissipate
-import Mathlib.Topology.Compactness.Compact
+import Mathlib.Topology.Separation.Hausdorff
 import Mathlib.MeasureTheory.PiSystem
 
+/-!
+# Compact systems.
+
+This files defines compact systems of sets.
+
+## 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.
+
+## Main results
+
+* `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.
+
+-/
+
 open Set Finset Nat
 
 section definition
@@ -16,7 +34,7 @@ variable {α : Type*} {p : Set α → Prop} {C : ℕ → Set α}
 /-- 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. -/
 def IsCompactSystem (p : Set α → Prop) : Prop :=
-  ∀ C : ℕ → Set α, (∀ i, p (C i)) → ⋂ i, C i = ∅ → ∃ (n : ℕ), ⋂ i ≤ n, C i = ∅
+  ∀ C : ℕ → Set α, (∀ i, p (C i)) → ⋂ i, C i = ∅ → ∃ (n : ℕ), Dissipate C n = ∅
 
 /-- In a compact system, given a countable family with empty intersection, we choose a finite
 subfamily with empty intersection-/
@@ -27,26 +45,19 @@ def IsCompactSystem.max_of_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i))
 
 lemma IsCompactSystem.iInter_eq_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i))
     (hC_empty : ⋂ i, C i = ∅) :
-    ⋂ i ≤ hp.max_of_empty hC hC_empty, C i = ∅ :=
+    Dissipate C (hp.max_of_empty hC hC_empty) = ∅ :=
   (hp C hC hC_empty).choose_spec
 
-theorem IsCompactSystem_iff_of_nempty (p : Set α → Prop) :
+theorem IsCompactSystem.iff_of_nempty (p : Set α → Prop) :
     IsCompactSystem p ↔ (∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ (n : ℕ),
-      (⋂ i ≤ n, C i).Nonempty) → (⋂ i, C i).Nonempty) := by
+      (Dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) := by
   refine ⟨fun h C hC hn ↦ ?_, fun h C hC ↦ ?_⟩ <;> have h2 := not_imp_not.mpr <| h C hC
   · push_neg at h2
     exact h2 hn
   · push_neg at h2
     exact h2
 
-lemma prime (C : Set (Set α)) (hC : ∅ ∈ C) : (IsPiSystem C) ↔ (∀ s ∈ C, ∀ t ∈ C, s ∩ t ∈ C) := by
-  refine ⟨fun h s hs t ht ↦ ?_, fun h s hs t ht _ ↦ h s hs t ht⟩
-  by_cases h' : (s ∩ t).Nonempty
-  · exact h s hs t ht h'
-  · push_neg at h'
-    exact h' ▸ hC
-
-theorem IsCompactSystem.iff_mono [Inhabited α] (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
+theorem IsCompactSystem.iff_directed (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
     (IsCompactSystem p) ↔
     (∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
       ⋂ i, C i = ∅ → ∃ (n : ℕ), C n = ∅) := by
@@ -56,29 +67,21 @@ theorem IsCompactSystem.iff_mono [Inhabited α] (hpi : ∀ (s t : Set α), p s 
   · rw [← biInter_le_eq_iInter] at h2
     exact h (Dissipate C) dissipate_directed (dissipate_of_piSystem hpi h1) h2
 
-theorem IsCompactSystem.iff_mono' [Inhabited α] (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
+theorem IsCompactSystem.iff_directed' (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
     (IsCompactSystem p) ↔
     ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
     (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty  := by
-  rw [IsCompactSystem.iff_mono hpi]
+  rw [IsCompactSystem.iff_directed hpi]
   refine ⟨fun h1 C h3 h4 ↦ ?_, fun h1 C h3 s ↦ ?_⟩ <;> rw [← not_imp_not] <;> push_neg
   · exact h1 C h3 h4
   · exact h1 C h3 s
 
 end definition
 
-section Compact
-
-variable {α : Type*}
-
-variable {α : Type*} [TopologicalSpace α]
-
-example (s t : Set α) (hs : IsClosed s) (ht : IsClosed t) : IsClosed (s ∩ t) := by
-  exact IsClosed.inter hs ht
+section ClosedCompact
 
-example : IsCompact (∅ : Set α) := by exact isCompact_empty
-
-theorem IsClosedCompact.isCompactSystem {α : Type*} [Inhabited α] [TopologicalSpace α] :
+/-- The set of compact and closed sets is a compact system. -/
+theorem IsClosedCompact.isCompactSystem {α : Type*} [TopologicalSpace α] :
     IsCompactSystem (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by
   have h : IsPiSystem ({ s : Set α | IsCompact s ∧ IsClosed s}) := by
     intro x hx y hy _
@@ -88,263 +91,22 @@ theorem IsClosedCompact.isCompactSystem {α : Type*} [Inhabited α] [Topological
   have h2 : ∀ (s t : Set α), IsCompact s ∧ IsClosed s →
       IsCompact t ∧ IsClosed t → IsCompact (s ∩ t) ∧ IsClosed (s ∩ t) :=
     fun s t h1 h2 ↦ ⟨IsCompact.inter_right h1.1 h2.2, IsClosed.inter h1.2 h2.2⟩
-  rw [prime _ h1] at h
-  rw [IsCompactSystem.iff_mono' h2]
+  rw [IsPiSystem.iff_of_empty_mem _ h1] at h
+  rw [IsCompactSystem.iff_directed' h2]
   exact fun s hs h1 h2 ↦ IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed s hs h2
     (fun i ↦ (h1 i).1) (fun i ↦ (h1 i).2)
 
-end Compact
-
-/--
-section ClosedCompactCylinders
-
-/-! We prove that the `closedCompactCylinders` are a compact system. -/
-
-variable {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i)] {s : ℕ → Set (Π i, α i)}
-
-local notation "Js" => closedCompactCylinders.finset
-local notation "As" => closedCompactCylinders.set
-
-section AllProj
-
-/-- All indices in `ι` that are constrained by the condition `∀ n, s n ∈ closedCompactCylinders α`.
-That is, the union of all indices in the bases of the cylinders. -/
-def allProj (hs : ∀ n, s n ∈ closedCompactCylinders α) : Set ι := ⋃ n, Js (hs n)
-
-theorem subset_allProj (hs : ∀ n, s n ∈ closedCompactCylinders α) (n : ℕ) :
-    ↑(Js (hs n)) ⊆ allProj hs :=
-  subset_iUnion (fun i ↦ (Js (hs i) : Set ι)) n
-
-theorem exists_nat_proj (hs : ∀ n, s n ∈ closedCompactCylinders α) (i : ι) (hi : i ∈ allProj hs) :
-    ∃ n, i ∈ Js (hs n) := by
-  simpa only [allProj, mem_iUnion, Finset.mem_coe] using hi
-
-open Classical in
-/-- The smallest `n` such that `i ∈ Js (hs n)`. That is, the first `n` such that `i` belongs to the
-finset defining the cylinder for `s n`. -/
-noncomputable def indexProj (hs : ∀ n, s n ∈ closedCompactCylinders α) (i : allProj hs) : ℕ :=
-  Nat.find (exists_nat_proj hs i i.2)
-
-open Classical in
-theorem mem_indexProj (hs : ∀ n, s n ∈ closedCompactCylinders α) (i : allProj hs) :
-    (i : ι) ∈ Js (hs (indexProj hs i)) :=
-  Nat.find_spec (exists_nat_proj hs i i.2)
-
-open Classical in
-theorem indexProj_le (hs : ∀ n, s n ∈ closedCompactCylinders α) (n : ℕ) (i : Js (hs n)) :
-    indexProj hs ⟨i, subset_allProj hs n i.2⟩ ≤ n :=
-  Nat.find_le i.2
+theorem IsCompact.isCompactSystem {α : Type*} [TopologicalSpace α]
+    (h : ∀ {s : Set α}, IsCompact s → IsClosed s) :
+    IsCompactSystem (fun s : Set α ↦ IsCompact s) := by
+  have h : (fun s : Set α ↦ IsCompact s) = (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by
+    ext s
+    refine ⟨fun h' ↦ ⟨h', h h'⟩, fun h' ↦ h'.1⟩
+  exact h ▸ IsClosedCompact.isCompactSystem
 
-lemma surjective_proj_allProj [∀ i, Nonempty (α i)] (hs : ∀ n, s n ∈ closedCompactCylinders α) :
-    Function.Surjective (fun (f : (Π i, α i)) (i : allProj hs) ↦ f (i : ι)) := by
-  intro y
-  let x := (inferInstance : Nonempty (Π i, α i)).some
-  classical
-  refine ⟨fun i ↦ if hi : i ∈ allProj hs then y ⟨i, hi⟩ else x i, ?_⟩
-  ext i
-  simp only [Subtype.coe_prop, dite_true]
+/-- In a `T2Space` The set of compact sets is a compact system. -/
+theorem IsCompact.isCompactSystem_of_T2Space {α : Type*} [TopologicalSpace α] [T2Space α] :
+    IsCompactSystem (fun s : Set α ↦ IsCompact s) :=
+  IsCompact.isCompactSystem fun {_} a ↦ isClosed a
 
-end AllProj
-
-section projCylinder
-
-/-- Given a countable family of closed cylinders, consider one of them as depending only on
-the countably many coordinates that appear in all of them. -/
-def projCylinder (hs : ∀ n, s n ∈ closedCompactCylinders α) (n : ℕ) :
-    Set (∀ i : allProj hs, α i) :=
-  (fun (f : ∀ i : allProj hs, α i) (i : Js (hs n)) ↦ f ⟨i, subset_allProj hs _ i.2⟩) ⁻¹' (As (hs n))
-
-lemma mem_projCylinder (hs : ∀ n, s n ∈ closedCompactCylinders α) (n : ℕ)
-    (x : ∀ i : allProj hs, α i) :
-    x ∈ projCylinder hs n ↔ (fun (i : Js (hs n)) ↦ x ⟨i, subset_allProj hs _ i.2⟩) ∈ As (hs n) := by
-  simp only [projCylinder, mem_preimage]
-
-theorem preimage_projCylinder (hs : ∀ n, s n ∈ closedCompactCylinders α) (n : ℕ) :
-    (fun (f : ∀ i, α i) (i : allProj hs) ↦ f i) ⁻¹' (projCylinder hs n) = s n := by
-  conv_rhs => rw [closedCompactCylinders.eq_cylinder (hs n)]
-  rfl
-
-lemma nonempty_projCylinder (hs : ∀ n, s n ∈ closedCompactCylinders α)
-    (n : ℕ) (hs_nonempty : (s n).Nonempty) :
-    (projCylinder hs n).Nonempty := by
-  rw [← preimage_projCylinder hs n] at hs_nonempty
-  exact nonempty_of_nonempty_preimage hs_nonempty
-
-lemma nonempty_projCylinder_iff [∀ i, Nonempty (α i)]
-    (hs : ∀ n, s n ∈ closedCompactCylinders α) (n : ℕ) :
-    (projCylinder hs n).Nonempty ↔ (s n).Nonempty := by
-  refine ⟨fun h ↦ ?_, nonempty_projCylinder hs n⟩
-  obtain ⟨x, hx⟩ := h
-  rw [mem_projCylinder] at hx
-  rw [closedCompactCylinders.eq_cylinder (hs n), MeasureTheory.cylinder]
-  refine Set.Nonempty.preimage ?_ ?_
-  · exact ⟨_, hx⟩
-  · intro y
-    let x := (inferInstance : Nonempty (∀ i, α i)).some
-    classical
-    refine ⟨fun i ↦ if hi : i ∈ Js (hs n) then y ⟨i, hi⟩ else x i, ?_⟩
-    ext i
-    simp only [Finset.restrict_def, Finset.coe_mem, dite_true]
-
-theorem isClosed_projCylinder
-    (hs : ∀ n, s n ∈ closedCompactCylinders α) (hs_closed : ∀ n, IsClosed (As (hs n))) (n : ℕ) :
-    IsClosed (projCylinder hs n) :=
-  (hs_closed n).preimage (by exact continuous_pi (fun i ↦ continuous_apply _))
-
-end projCylinder
-
-section piCylinderSet
-
-open Classical in
-/-- Given countably many closed compact cylinders, the product set which, in each relevant
-coordinate, is the projection of the first cylinder for which this coordinate is relevant. -/
-def piCylinderSet (hs : ∀ n, s n ∈ closedCompactCylinders α) :
-    Set (∀ i : allProj hs, α i) :=
-  {x : ∀ i : allProj hs, α i |
-    ∀ i, x i ∈ (fun a : ∀ j : Js (hs (indexProj hs i)), α j ↦ a ⟨i, mem_indexProj hs i⟩) ''
-      (As (hs (indexProj hs i)))}
-
-lemma mem_piCylinderSet (hs : ∀ n, s n ∈ closedCompactCylinders α)
-    (x : ∀ i : allProj hs, α i) :
-    x ∈ piCylinderSet hs ↔
-    ∀ i, x i ∈ (fun a : ∀ j : Js (hs (indexProj hs i)), α j ↦ a ⟨i, mem_indexProj hs i⟩) ''
-      (As (hs (indexProj hs i))) := by
-  simp only [piCylinderSet, mem_image, Subtype.forall, mem_setOf_eq]
-
-theorem isCompact_piCylinderSet (hs : ∀ n, s n ∈ closedCompactCylinders α) :
-    IsCompact (piCylinderSet hs) :=
-  isCompact_pi_infinite fun _ ↦
-    (closedCompactCylinders.isCompact (hs _)).image (continuous_apply _)
-
-theorem piCylinderSet_eq_pi_univ (hs : ∀ n, s n ∈ closedCompactCylinders α) :
-    piCylinderSet hs =
-      pi univ fun i ↦
-        (fun a : ∀ j : Js (hs (indexProj hs i)), α j ↦ a ⟨i, mem_indexProj hs i⟩) ''
-          (As (hs (indexProj hs i))) := by
-  ext; simp only [piCylinderSet, mem_univ_pi]; rfl
-
-theorem isClosed_piCylinderSet (hs : ∀ n, s n ∈ closedCompactCylinders α) :
-    IsClosed (piCylinderSet hs) := by
-  rw [piCylinderSet_eq_pi_univ]
-  exact isClosed_set_pi fun i _ ↦ IsClosed.isClosed_image_restrict_singleton _
-    (closedCompactCylinders.isCompact (hs _)) (closedCompactCylinders.isClosed (hs _))
-
-theorem nonempty_piCylinderSet (hs : ∀ n, s n ∈ closedCompactCylinders α)
-    (hs_nonempty : ∀ i, (s i).Nonempty) :
-    (piCylinderSet hs).Nonempty := by
-  have hs_nonempty' i : (As (hs i)).Nonempty := by
-    specialize hs_nonempty i
-    rw [closedCompactCylinders.eq_cylinder (hs i)] at hs_nonempty
-    exact nonempty_of_nonempty_preimage hs_nonempty
-  let b i := (hs_nonempty' (indexProj hs i)).some
-  have hb_mem i : b i ∈ As (hs (indexProj hs i)) := (hs_nonempty' (indexProj hs i)).choose_spec
-  let a : ∀ i : allProj hs, α i := fun i ↦ b i ⟨i, mem_indexProj hs i⟩
-  refine ⟨a, ?_⟩
-  simp only [piCylinderSet, mem_image, SetCoe.forall, mem_setOf_eq]
-  exact fun j hj ↦ ⟨b ⟨j, hj⟩, hb_mem _, rfl⟩
-
-end piCylinderSet
-
-theorem iInter_subset_piCylinderSet (hs : ∀ n, s n ∈ closedCompactCylinders α) :
-    (⋂ n, projCylinder hs n) ⊆ piCylinderSet hs := by
-  intro x hx
-  rw [mem_iInter] at hx
-  rw [mem_piCylinderSet]
-  intro i
-  specialize hx (indexProj hs i)
-  rw [mem_projCylinder] at hx
-  exact ⟨fun i : Js (hs (indexProj hs i)) ↦ x ⟨i, subset_allProj hs _ i.2⟩, hx, rfl⟩
-
-theorem nonempty_iInter_projCylinder_inter_piCylinderSet (hs : ∀ n, s n ∈ closedCompactCylinders α)
-    (hs_nonempty : ∀ i, (s i).Nonempty)
-    (h_nonempty : ∀ n, (⋂ i ≤ n, projCylinder hs i).Nonempty) (n : ℕ) :
-    ((⋂ i ≤ n, projCylinder hs i) ∩ piCylinderSet hs).Nonempty := by
-  obtain ⟨x, hx⟩ := nonempty_piCylinderSet hs hs_nonempty
-  obtain ⟨y, hy⟩ := h_nonempty n
-  let z := fun i : allProj hs ↦ if indexProj hs i ≤ n then y i else x i
-  refine ⟨z, mem_inter ?_ ?_⟩
-  · simp only [mem_iInter, mem_projCylinder]
-    intro i hi
-    have : (fun j : Js (hs i) ↦
-          ite (indexProj hs ⟨j, subset_allProj hs i j.2⟩ ≤ n) (y ⟨j, subset_allProj hs i j.2⟩)
-            (x ⟨j, subset_allProj hs i j.2⟩)) =
-        fun j : Js (hs i) ↦ y ⟨j, subset_allProj hs i j.2⟩ := by
-      ext j
-      rw [if_pos]
-      refine le_trans (le_of_eq ?_) ((indexProj_le hs i j).trans hi)
-      congr
-    rw [this]
-    have hyi : y ∈ projCylinder hs i := by
-      suffices ⋂ j ≤ n, projCylinder hs j ⊆ projCylinder hs i by exact this hy
-      exact biInter_subset_of_mem hi
-    rwa [mem_projCylinder] at hyi
-  · rw [mem_piCylinderSet]
-    intro i
-    by_cases hi_le : indexProj hs i ≤ n
-    · let m := indexProj hs i
-      have hy' : y ∈ projCylinder hs m := by
-        suffices ⋂ j ≤ n, projCylinder hs j ⊆ projCylinder hs m by exact this hy
-        exact biInter_subset_of_mem hi_le
-      rw [mem_projCylinder] at hy'
-      refine ⟨fun j ↦ y ⟨j, subset_allProj hs _ j.2⟩, hy', ?_⟩
-      simp_rw [z, if_pos hi_le]
-    · rw [mem_piCylinderSet] at hx
-      specialize hx i
-      obtain ⟨x', hx'_mem, hx'_eq⟩ := hx
-      refine ⟨x', hx'_mem, ?_⟩
-      simp_rw [z, if_neg hi_le]
-      exact hx'_eq
-
-theorem nonempty_iInter_projCylinder (hs : ∀ n, s n ∈ closedCompactCylinders α)
-    (hs_nonempty : ∀ i, (s i).Nonempty)
-    (h_nonempty : ∀ n, (⋂ i ≤ n, projCylinder hs i).Nonempty) :
-    (⋂ i, projCylinder hs i).Nonempty := by
-  suffices ((⋂ i, projCylinder hs i) ∩ piCylinderSet hs).Nonempty by
-    rwa [inter_eq_left.mpr (iInter_subset_piCylinderSet hs)] at this
-  have : (⋂ n, projCylinder hs n) = (⋂ n, ⋂ i ≤ n, projCylinder hs i) := by
-    ext x
-    simp only [mem_iInter]
-    exact ⟨fun h i j _ ↦ h j, fun h i ↦ h i i le_rfl⟩
-  rw [this, iInter_inter]
-  have h_closed : ∀ n, IsClosed (⋂ i ≤ n, projCylinder hs i) :=
-    fun n ↦ isClosed_biInter (fun i _ ↦ isClosed_projCylinder hs
-      (fun n ↦ (closedCompactCylinders.isClosed (hs n))) i)
-  refine IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
-    (fun n ↦ (⋂ i ≤ n, projCylinder hs i) ∩ piCylinderSet hs) ?_ ?_ ?_ ?_
-  · refine fun i ↦ inter_subset_inter ?_ subset_rfl
-    simp_rw [Set.biInter_le_succ]
-    exact inter_subset_left
-  · exact fun n ↦ nonempty_iInter_projCylinder_inter_piCylinderSet hs hs_nonempty h_nonempty n
-  · exact (isCompact_piCylinderSet hs).inter_left (h_closed _)
-  · exact fun n ↦ IsClosed.inter (h_closed n) (isClosed_piCylinderSet hs)
-
-lemma exists_finset_iInter_projCylinder_eq_empty [∀ i, Nonempty (α i)]
-    (hs : ∀ n, s n ∈ closedCompactCylinders α) (h : ⋂ n, projCylinder hs n = ∅) :
-    ∃ t : Finset ℕ, (⋂ i ∈ t, projCylinder hs i) = ∅ := by
-  by_contra! h_nonempty
-  refine absurd h (Set.Nonempty.ne_empty ?_)
-  refine nonempty_iInter_projCylinder hs (fun i ↦ ?_) (fun n ↦ ?_)
-  · specialize h_nonempty {i}
-    simp only [Finset.mem_singleton, iInter_iInter_eq_left, ne_eq] at h_nonempty
-    rwa [nonempty_projCylinder_iff] at h_nonempty
-  · specialize h_nonempty (Finset.range (n + 1))
-    simp only [Finset.mem_range, ne_eq, Nat.lt_succ_iff] at h_nonempty
-    exact h_nonempty
-
-/-- The `closedCompactCylinders` are a compact system. -/
-theorem isCompactSystem_closedCompactCylinders : IsCompactSystem (closedCompactCylinders α) := by
-  intro s hs h
-  by_cases hα : ∀ i, Nonempty (α i)
-  swap; · exact ⟨∅, by simpa [not_nonempty_iff] using hα⟩
-  have h' : ⋂ n, projCylinder hs n = ∅ := by
-    simp_rw [← preimage_projCylinder hs, ← preimage_iInter] at h
-    have h_surj : Function.Surjective (fun (f : (∀ i, α i)) (i : allProj hs) ↦ f (i : ι)) :=
-      surjective_proj_allProj hs
-    rwa [← not_nonempty_iff_eq_empty, ← Function.Surjective.nonempty_preimage h_surj,
-      not_nonempty_iff_eq_empty]
-  obtain ⟨t, ht⟩ := exists_finset_iInter_projCylinder_eq_empty hs h'
-  refine ⟨t, ?_⟩
-  simp_rw [← preimage_projCylinder hs, ← preimage_iInter₂, ht, preimage_empty]
-
-end ClosedCompactCylinders
--/
+end ClosedCompact

From 384af7419012e2f316b3d496b79a9036e6a127ff Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Sat, 8 Mar 2025 22:17:12 +0100
Subject: [PATCH 16/53] merge master

---
 .../Topology/Compactness/CompactSystem.lean   | 22 +++++++++++--------
 1 file changed, 13 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index bae79df4393bf8..0c6b64c689b12d 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -27,28 +27,32 @@ This files defines compact systems of sets.
 
 open Set Finset Nat
 
-section definition
-
 variable {α : Type*} {p : Set α → Prop} {C : ℕ → Set α}
 
+section definition
+
 /-- 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. -/
 def IsCompactSystem (p : Set α → Prop) : Prop :=
   ∀ C : ℕ → Set α, (∀ i, p (C i)) → ⋂ i, C i = ∅ → ∃ (n : ℕ), Dissipate C n = ∅
 
+end definition
+
+namespace IsCompactSystem
+
 /-- In a compact system, given a countable family with empty intersection, we choose a finite
-subfamily with empty intersection-/
+subfamily with empty intersection. -/
 noncomputable
-def IsCompactSystem.max_of_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i))
+def max_of_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i))
     (hC_empty : ⋂ i, C i = ∅) : ℕ :=
   (hp C hC hC_empty).choose
 
-lemma IsCompactSystem.iInter_eq_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i))
+lemma iInter_eq_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i))
     (hC_empty : ⋂ i, C i = ∅) :
     Dissipate C (hp.max_of_empty hC hC_empty) = ∅ :=
   (hp C hC hC_empty).choose_spec
 
-theorem IsCompactSystem.iff_of_nempty (p : Set α → Prop) :
+theorem iff_of_nempty (p : Set α → Prop) :
     IsCompactSystem p ↔ (∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ (n : ℕ),
       (Dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) := by
   refine ⟨fun h C hC hn ↦ ?_, fun h C hC ↦ ?_⟩ <;> have h2 := not_imp_not.mpr <| h C hC
@@ -57,7 +61,7 @@ theorem IsCompactSystem.iff_of_nempty (p : Set α → Prop) :
   · push_neg at h2
     exact h2
 
-theorem IsCompactSystem.iff_directed (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
+theorem iff_directed (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
     (IsCompactSystem p) ↔
     (∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
       ⋂ i, C i = ∅ → ∃ (n : ℕ), C n = ∅) := by
@@ -67,7 +71,7 @@ theorem IsCompactSystem.iff_directed (hpi : ∀ (s t : Set α), p s → p t →
   · rw [← biInter_le_eq_iInter] at h2
     exact h (Dissipate C) dissipate_directed (dissipate_of_piSystem hpi h1) h2
 
-theorem IsCompactSystem.iff_directed' (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
+theorem iff_directed' (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
     (IsCompactSystem p) ↔
     ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
     (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty  := by
@@ -76,7 +80,7 @@ theorem IsCompactSystem.iff_directed' (hpi : ∀ (s t : Set α), p s → p t →
   · exact h1 C h3 h4
   · exact h1 C h3 s
 
-end definition
+end IsCompactSystem
 
 section ClosedCompact
 

From a81f3d8ede760e9816b22d54d0efeba524c1a300 Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Tue, 11 Mar 2025 22:29:15 +0100
Subject: [PATCH 17/53] added or univ

---
 .../Topology/Compactness/CompactSystem.lean   | 84 ++++++++++++++-----
 1 file changed, 62 insertions(+), 22 deletions(-)

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 0c6b64c689b12d..122bcf8e565282 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -21,8 +21,7 @@ This files defines compact systems of sets.
 
 * `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.
-
+  is a compact system in a `T2Space`.
 -/
 
 open Set Finset Nat
@@ -80,37 +79,78 @@ theorem iff_directed' (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
   · exact h1 C h3 h4
   · exact h1 C h3 s
 
-end IsCompactSystem
+/-- Any subset of a compact system is a compact system. -/
+theorem of_supset {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
+
 
 section ClosedCompact
 
-/-- The set of compact and closed sets is a compact system. -/
-theorem IsClosedCompact.isCompactSystem {α : Type*} [TopologicalSpace α] :
-    IsCompactSystem (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by
-  have h : IsPiSystem ({ s : Set α | IsCompact s ∧ IsClosed s}) := by
-    intro x hx y hy _
-    exact ⟨IsCompact.inter_left hy.1 hx.2, IsClosed.inter hx.2 hy.2 ⟩
-  have h1 : ∅ ∈ {s : Set α| IsCompact s ∧ IsClosed s} := by
-    exact ⟨isCompact_empty, isClosed_empty⟩
-  have h2 : ∀ (s t : Set α), IsCompact s ∧ IsClosed s →
-      IsCompact t ∧ IsClosed t → IsCompact (s ∩ t) ∧ IsClosed (s ∩ t) :=
-    fun s t h1 h2 ↦ ⟨IsCompact.inter_right h1.1 h2.2, IsClosed.inter h1.2 h2.2⟩
-  rw [IsPiSystem.iff_of_empty_mem _ h1] at h
+/-- The set of sets which are either compact and closed, or `univ`, is a compact system. -/
+theorem of_isClosedCompactOrUniv {α : Type*} [TopologicalSpace α] :
+    IsCompactSystem (fun s : Set α ↦ (IsCompact s ∧ IsClosed s) ∨ (s = univ)) := by
+  let p := fun (s : Set α) ↦ (IsCompact s ∧ IsClosed s) ∨ (s = univ)
+  have h2 : ∀ (s t : Set α), p s → p t → p (s ∩ t) := by
+    intro s t hs ht
+    by_cases hs' : s = univ
+    · rw [hs', univ_inter]
+      exact ht
+    · by_cases ht' : t = univ
+      · rw [ht', inter_comm, univ_inter]
+        exact hs
+      · exact Or.inl <| ⟨IsCompact.inter_right (Or.resolve_right hs hs').1
+        (Or.resolve_right ht ht').2, IsClosed.inter (Or.resolve_right hs hs').2
+          (Or.resolve_right ht ht').2⟩
   rw [IsCompactSystem.iff_directed' h2]
-  exact fun s hs h1 h2 ↦ IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed s hs h2
-    (fun i ↦ (h1 i).1) (fun i ↦ (h1 i).2)
+  intro s hs h1 h2
+  let s' := fun (i : { j : ℕ | s j ≠ univ}) ↦ s i
+  have hs' : Directed (fun x1 x2 ↦ x1 ⊇ x2) s' := by
+    intro a b
+    obtain ⟨z, hz1, hz2⟩ := hs a.val b.val
+    have hz : s z ≠ univ := fun h ↦ a.prop <| eq_univ_of_subset hz1 h
+    use ⟨z, hz⟩
+  have htcl : ∀ (i : { j : ℕ | s j ≠ univ}), IsClosed (s i) :=
+    fun i ↦ (Or.resolve_right (h1 i.val) i.prop).2
+  have htco : ∀ (i : { j : ℕ | s j ≠ univ}), IsCompact (s i) :=
+    fun i ↦ (Or.resolve_right (h1 i.val) i.prop).1
+  haveI f : Nonempty α := by
+    apply nonempty_of_exists _
+    · exact fun x ↦ x ∈ s 0
+    · exact h2 0
+  by_cases h : Nonempty ↑{j | s j ≠ Set.univ}
+  · have g :  (⋂ i, s' i).Nonempty → (⋂ i, s i).Nonempty := by
+      rw [Set.nonempty_iInter, Set.nonempty_iInter]
+      rintro ⟨x, hx⟩
+      use x
+      intro i
+      by_cases g : s i ≠ univ
+      · exact hx ⟨i, g⟩
+      · simp only [ne_eq, not_not, s'] at g
+        rw [g]
+        simp only [Set.mem_univ]
+    apply g <| IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed s' hs'
+      (fun j ↦ h2 j) htco htcl
+  · simp only [ne_eq, coe_setOf, nonempty_subtype, not_exists, not_not, s'] at h
+    simp only [nonempty_iInter, s', h]
+    simp only [Set.mem_univ, implies_true, exists_const, s']
 
-theorem IsCompact.isCompactSystem {α : Type*} [TopologicalSpace α]
+/-- The set of compact and closed sets is a compact system. -/
+theorem of_isClosedCompact {α : Type*} [TopologicalSpace α] :
+    IsCompactSystem (fun s : Set α ↦ IsCompact s ∧ IsClosed s) :=
+  IsCompactSystem.of_supset of_isClosedCompactOrUniv (fun _ hs ↦ Or.inl hs)
+
+theorem of_isCompact {α : Type*} [TopologicalSpace α]
     (h : ∀ {s : Set α}, IsCompact s → IsClosed s) :
     IsCompactSystem (fun s : Set α ↦ IsCompact s) := by
   have h : (fun s : Set α ↦ IsCompact s) = (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by
     ext s
     refine ⟨fun h' ↦ ⟨h', h h'⟩, fun h' ↦ h'.1⟩
-  exact h ▸ IsClosedCompact.isCompactSystem
+  exact h ▸ of_isClosedCompact
 
 /-- In a `T2Space` The set of compact sets is a compact system. -/
-theorem IsCompact.isCompactSystem_of_T2Space {α : Type*} [TopologicalSpace α] [T2Space α] :
-    IsCompactSystem (fun s : Set α ↦ IsCompact s) :=
-  IsCompact.isCompactSystem fun {_} a ↦ isClosed a
+theorem _of_isCompact_of_T2Space {α : Type*} [TopologicalSpace α] [T2Space α] :
+    IsCompactSystem (fun s : Set α ↦ IsCompact s) := of_isCompact (fun hs ↦ hs.isClosed)
 
 end ClosedCompact
+
+end IsCompactSystem

From 16b754e9e1fe321153f360c64c1d38bd04ac1d07 Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Wed, 19 Mar 2025 22:57:19 +0100
Subject: [PATCH 18/53] in line with pfaffelh_compactSystem2

---
 Mathlib/Topology/Compactness/CompactSystem.lean | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 122bcf8e565282..cefdde851d2789 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -86,8 +86,10 @@ theorem of_supset {C D : (Set α) → Prop} (hD : IsCompactSystem D) (hCD : ∀
 
 section ClosedCompact
 
+variable (α : Type*) [TopologicalSpace α]
+
 /-- The set of sets which are either compact and closed, or `univ`, is a compact system. -/
-theorem of_isClosedCompactOrUniv {α : Type*} [TopologicalSpace α] :
+theorem isClosedCompactOrUnivs :
     IsCompactSystem (fun s : Set α ↦ (IsCompact s ∧ IsClosed s) ∨ (s = univ)) := by
   let p := fun (s : Set α) ↦ (IsCompact s ∧ IsClosed s) ∨ (s = univ)
   have h2 : ∀ (s t : Set α), p s → p t → p (s ∩ t) := by
@@ -135,21 +137,20 @@ theorem of_isClosedCompactOrUniv {α : Type*} [TopologicalSpace α] :
     simp only [Set.mem_univ, implies_true, exists_const, s']
 
 /-- The set of compact and closed sets is a compact system. -/
-theorem of_isClosedCompact {α : Type*} [TopologicalSpace α] :
+theorem isClosedCompacts :
     IsCompactSystem (fun s : Set α ↦ IsCompact s ∧ IsClosed s) :=
-  IsCompactSystem.of_supset of_isClosedCompactOrUniv (fun _ hs ↦ Or.inl hs)
+  IsCompactSystem.of_supset (isClosedCompactOrUnivs α) (fun _ hs ↦ Or.inl hs)
 
-theorem of_isCompact {α : Type*} [TopologicalSpace α]
-    (h : ∀ {s : Set α}, IsCompact s → IsClosed s) :
+theorem isCompacts (h : ∀ {s : Set α}, IsCompact s → IsClosed s) :
     IsCompactSystem (fun s : Set α ↦ IsCompact s) := by
   have h : (fun s : Set α ↦ IsCompact s) = (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by
     ext s
     refine ⟨fun h' ↦ ⟨h', h h'⟩, fun h' ↦ h'.1⟩
-  exact h ▸ of_isClosedCompact
+  exact h ▸ (isClosedCompacts α)
 
 /-- In a `T2Space` The set of compact sets is a compact system. -/
-theorem _of_isCompact_of_T2Space {α : Type*} [TopologicalSpace α] [T2Space α] :
-    IsCompactSystem (fun s : Set α ↦ IsCompact s) := of_isCompact (fun hs ↦ hs.isClosed)
+theorem _of_isCompact_of_T2Space [T2Space α] :
+    IsCompactSystem (fun s : Set α ↦ IsCompact s) := (isCompacts α) (fun hs ↦ hs.isClosed)
 
 end ClosedCompact
 

From 6fced3f6c175ae52a7999437361c547cd60c80fa Mon Sep 17 00:00:00 2001
From: pfaffelh <p.p@stochastik.uni-freiburg.de>
Date: Wed, 30 Apr 2025 22:44:11 +0200
Subject: [PATCH 19/53] added iff

---
 .../Topology/Compactness/CompactSystem.lean   | 30 +++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index cefdde851d2789..eb069a20e22b28 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -39,6 +39,36 @@ end definition
 
 namespace IsCompactSystem
 
+lemma iff (p : Set α → Prop) : IsCompactSystem p ↔
+    ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, ⋂ k < n, C k ≠ ∅) → ⋂ i, C i ≠ ∅ := by
+  refine ⟨fun h C hi ↦ ?_, fun h C hi ↦ ?_⟩
+  · rw [← not_imp_not]
+    push_neg
+    intro h'
+    specialize h C hi h'
+    obtain ⟨n, hn⟩ := h
+    use n + 1
+    rw [Dissipate] at hn
+    conv =>
+      lhs
+      enter [1]
+      intro j
+      rw [Nat.lt_add_one_iff]
+    exact hn
+  · rw [← not_imp_not]
+    push_neg
+    simp_rw [nonempty_iff_ne_empty]
+    intro h'
+    apply h C hi
+    intro n hn
+    apply h' n
+    rw [← subset_empty_iff] at hn ⊢
+    apply le_trans _ hn
+    rw [Dissipate]
+    intro x
+    rw [mem_iInter₂, mem_iInter₂]
+    exact fun h i hi ↦ h i hi.le
+
 /-- In a compact system, given a countable family with empty intersection, we choose a finite
 subfamily with empty intersection. -/
 noncomputable

From 8765264559c2113b085458e3f894bb8f62fbf504 Mon Sep 17 00:00:00 2001
From: pfaffelh <p.p@stochastik.uni-freiburg.de>
Date: Wed, 30 Apr 2025 23:41:16 +0200
Subject: [PATCH 20/53] n

---
 Mathlib/Data/Set/Dissipate.lean               |  4 ++
 .../Topology/Compactness/CompactSystem.lean   | 51 ++++++++-----------
 2 files changed, 24 insertions(+), 31 deletions(-)

diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean
index 403c6a14de6fd2..a618d5bd00d977 100644
--- a/Mathlib/Data/Set/Dissipate.lean
+++ b/Mathlib/Data/Set/Dissipate.lean
@@ -23,6 +23,10 @@ def Dissipate [LE α] (s : α → Set β) (x : α) : Set β :=
 @[simp]
 theorem dissipate_def [LE α] {x : α} : Dissipate s x = ⋂ y ≤ x, s y := rfl
 
+theorem dissipate_eq {s : ℕ → Set β} {n : ℕ} : Dissipate s n = ⋂ k < n + 1, s k := by
+  simp_rw [Nat.lt_add_one_iff]
+  rfl
+
 @[simp]
 theorem mem_dissipate [LE α] {x : α} {z : β} : z ∈ Dissipate s x ↔ ∀ y ≤ x, z ∈ s y := by
   simp_rw [dissipate_def, mem_iInter₂]
diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index eb069a20e22b28..5ab095b4cd49d4 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2023 Rémy Degenne. All rights reserved.
+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
 -/
@@ -39,36 +39,6 @@ end definition
 
 namespace IsCompactSystem
 
-lemma iff (p : Set α → Prop) : IsCompactSystem p ↔
-    ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, ⋂ k < n, C k ≠ ∅) → ⋂ i, C i ≠ ∅ := by
-  refine ⟨fun h C hi ↦ ?_, fun h C hi ↦ ?_⟩
-  · rw [← not_imp_not]
-    push_neg
-    intro h'
-    specialize h C hi h'
-    obtain ⟨n, hn⟩ := h
-    use n + 1
-    rw [Dissipate] at hn
-    conv =>
-      lhs
-      enter [1]
-      intro j
-      rw [Nat.lt_add_one_iff]
-    exact hn
-  · rw [← not_imp_not]
-    push_neg
-    simp_rw [nonempty_iff_ne_empty]
-    intro h'
-    apply h C hi
-    intro n hn
-    apply h' n
-    rw [← subset_empty_iff] at hn ⊢
-    apply le_trans _ hn
-    rw [Dissipate]
-    intro x
-    rw [mem_iInter₂, mem_iInter₂]
-    exact fun h i hi ↦ h i hi.le
-
 /-- In a compact system, given a countable family with empty intersection, we choose a finite
 subfamily with empty intersection. -/
 noncomputable
@@ -90,6 +60,25 @@ theorem iff_of_nempty (p : Set α → Prop) :
   · push_neg at h2
     exact h2
 
+/-- In this equivalent formulation for a compact system,
+note that we use `⋂ k < n, C k` rather than `⋂ k ≤ n, C k`. -/
+lemma iff_of_not_empty (p : Set α → Prop) : IsCompactSystem p ↔
+    ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, ⋂ k < n, C k ≠ ∅) → ⋂ i, C i ≠ ∅ := by
+  simp_rw [← Set.nonempty_iff_ne_empty, iff_of_nempty]
+  refine ⟨fun h C hi h'↦ ?_, fun h C hi h' ↦ ?_⟩
+  · apply h C hi
+    exact fun n ↦ dissipate_eq ▸ (h' (n + 1))
+  · apply h C hi
+    intro n
+    simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢
+    intro g
+    apply h' n
+    simp_rw [← subset_empty_iff, Dissipate] at g ⊢
+    apply le_trans _ g
+    intro x
+    rw [mem_iInter₂, mem_iInter₂]
+    exact fun h i hi ↦ h i hi.le
+
 theorem iff_directed (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
     (IsCompactSystem p) ↔
     (∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →

From 66d9abefd78a02bd7cda29c4c09bb5087635b860 Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Fri, 2 May 2025 08:14:21 +0200
Subject: [PATCH 21/53] update Mathlib

---
 Mathlib.lean                                    | 2 ++
 Mathlib/Topology/Compactness/CompactSystem.lean | 1 -
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index abab371c8b6976..c76078ec597e86 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3302,6 +3302,7 @@ import Mathlib.Data.Set.Constructions
 import Mathlib.Data.Set.Countable
 import Mathlib.Data.Set.Defs
 import Mathlib.Data.Set.Disjoint
+import Mathlib.Data.Set.Dissipate
 import Mathlib.Data.Set.Enumerate
 import Mathlib.Data.Set.Equitable
 import Mathlib.Data.Set.Finite.Basic
@@ -5951,6 +5952,7 @@ import Mathlib.Topology.Compactification.OnePointEquiv
 import Mathlib.Topology.Compactness.Bases
 import Mathlib.Topology.Compactness.Compact
 import Mathlib.Topology.Compactness.CompactlyGeneratedSpace
+import Mathlib.Topology.Compactness.CompactSystem
 import Mathlib.Topology.Compactness.DeltaGeneratedSpace
 import Mathlib.Topology.Compactness.Exterior
 import Mathlib.Topology.Compactness.Lindelof
diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 5ab095b4cd49d4..9722c003f2e701 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -102,7 +102,6 @@ theorem iff_directed' (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
 theorem of_supset {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
 
-
 section ClosedCompact
 
 variable (α : Type*) [TopologicalSpace α]

From 2ee5f258f64aa7d30c30f77463deb9a8dcc684ed Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Fri, 2 May 2025 09:29:05 +0200
Subject: [PATCH 22/53] linters dissipate

---
 Mathlib/Data/Set/Dissipate.lean | 20 ++++++++------------
 1 file changed, 8 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean
index a618d5bd00d977..da1a03f4593fc5 100644
--- a/Mathlib/Data/Set/Dissipate.lean
+++ b/Mathlib/Data/Set/Dissipate.lean
@@ -27,9 +27,8 @@ theorem dissipate_eq {s : ℕ → Set β} {n : ℕ} : Dissipate s n = ⋂ k < n
   simp_rw [Nat.lt_add_one_iff]
   rfl
 
-@[simp]
 theorem mem_dissipate [LE α] {x : α} {z : β} : z ∈ Dissipate s x ↔ ∀ y ≤ x, z ∈ s y := by
-  simp_rw [dissipate_def, mem_iInter₂]
+  simp only [dissipate_def, mem_iInter]
 
 theorem dissipate_subset [Preorder α] {x y : α} (hy : y ≤ x): Dissipate s x ⊆ s y :=
   biInter_subset_of_mem hy
@@ -46,7 +45,6 @@ theorem dissipate_subset_dissipate [Preorder α] {x y} (h : y ≤ x) :
     Dissipate s x ⊆ Dissipate s y :=
   antitone_dissipate h
 
-@[simp]
 theorem biInter_dissipate [Preorder α] {s : α → Set β} {x : α} :
     ⋂ y ≤ x, s y = ⋂ y ≤ x, ⋂ z ≤ y, s z := by
   apply Subset.antisymm
@@ -61,15 +59,14 @@ theorem iInter_dissipate [Preorder α] : ⋂ x, s x = ⋂ x, Dissipate s x := by
   · exact fun z h x' y hy ↦ h y
   · exact fun z h x' ↦ h x' x' (le_refl x')
 
-@[simp]
 lemma dissipate_bot [PartialOrder α] [OrderBot α] (s : α → Set β) : Dissipate s ⊥ = s ⊥ := by
-  simp [Set.dissipate_def]
+  simp only [dissipate_def, le_bot_iff, iInter_iInter_eq_left]
 
 open Nat
 
 @[simp]
 theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) :
-    Dissipate s (n + 1) = Dissipate s n ∩ s (n + 1) := by
+    ⋂ y, ⋂ (_ : y ≤ n + 1), s y = Dissipate s n ∩ s (n + 1) := by
   ext x
   refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
   · simp only [mem_inter_iff, mem_iInter, Dissipate] at *
@@ -82,7 +79,6 @@ theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) :
     · simp only [not_le] at h
       exact le_antisymm hi h ▸ hx.2
 
-@[simp]
 lemma dissipate_zero (s : ℕ → Set β) : Dissipate s 0 = s 0 := by
   simp [dissipate_def]
 
@@ -92,7 +88,7 @@ lemma subset_of_directed {s : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set 
   | zero => use 0; simp
   | succ n hn =>
     obtain ⟨m, hm⟩ := hn
-    simp_rw [← dissipate_def, dissipate_succ]
+    simp_rw [dissipate_succ]
     obtain ⟨k, hk⟩ := hd m (n+1)
     simp at hk
     use k
@@ -106,7 +102,7 @@ lemma empty_of_directed {s : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α
     · rw [hn']
       exact Eq.trans (dissipate_zero s) (hn' ▸ hn)
     · obtain ⟨k, hk⟩ := exists_eq_succ_of_ne_zero hn'
-      rw [hk, dissipate_succ, ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
+      rw [hk, dissipate_def, dissipate_succ, ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
   · rw [← not_imp_not]
     push_neg
     intro h n
@@ -124,7 +120,7 @@ lemma mem_subset_dissipate_of_directed (C : ℕ → Set α)
   | succ n hn =>
     obtain ⟨m, hm⟩ := hn
     obtain ⟨k, hk⟩ := hd m (n+1)
-    simp_rw [dissipate_succ]
+    simp_rw [dissipate_def, dissipate_succ]
     simp at hk
     exact ⟨k, Set.subset_inter_iff.mpr <| ⟨le_trans hk.1 hm, hk.2⟩⟩
 
@@ -136,7 +132,7 @@ lemma dissipate_exists_empty_iff_of_directed (C : ℕ → Set α)
     · rw [hn', dissipate_zero]
       exact hn' ▸ hn
     · obtain ⟨k, hk⟩ := exists_eq_succ_of_ne_zero hn'
-      simp_rw [hk, succ_eq_add_one, dissipate_succ,
+      simp_rw [hk, succ_eq_add_one, dissipate_def, dissipate_succ,
         ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
   · rw [← not_imp_not]
     push_neg
@@ -154,7 +150,7 @@ lemma dissipate_of_piSystem {s : ℕ → Set α} {p : Set α → Prop}
     simp only [dissipate_def, le_zero_eq, iInter_iInter_eq_left]
     exact h 0
   | succ n hn =>
-    rw [dissipate_succ]
+    rw [dissipate_def, dissipate_succ]
     exact hp (Dissipate s n) (s (n+1)) hn (h (n+1))
 
 end Set

From 383923b54ce49263d34e0c2c8f36e2fb010cbbc0 Mon Sep 17 00:00:00 2001
From: pfaffelh <p.p@stochastik.uni-freiburg.de>
Date: Fri, 2 May 2025 09:40:06 +0200
Subject: [PATCH 23/53] run mk_all

---
 Mathlib.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 1b1a3f6f97606a..a20ccfed98e707 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5953,8 +5953,8 @@ import Mathlib.Topology.Compactification.OnePoint
 import Mathlib.Topology.Compactification.OnePointEquiv
 import Mathlib.Topology.Compactness.Bases
 import Mathlib.Topology.Compactness.Compact
-import Mathlib.Topology.Compactness.CompactlyGeneratedSpace
 import Mathlib.Topology.Compactness.CompactSystem
+import Mathlib.Topology.Compactness.CompactlyGeneratedSpace
 import Mathlib.Topology.Compactness.DeltaGeneratedSpace
 import Mathlib.Topology.Compactness.Exterior
 import Mathlib.Topology.Compactness.Lindelof

From ab38ce2e7c671911e456d212be4ba3b951a37257 Mon Sep 17 00:00:00 2001
From: pfaffelh <p.p@stochastik.uni-freiburg.de>
Date: Fri, 2 May 2025 09:49:32 +0200
Subject: [PATCH 24/53] min imports

---
 Mathlib/Topology/Compactness/CompactSystem.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 9722c003f2e701..7f458db4e0d27b 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -5,7 +5,6 @@ Authors: Rémy Degenne, Peter Pfaffelhuber
 -/
 import Mathlib.Data.Set.Dissipate
 import Mathlib.Topology.Separation.Hausdorff
-import Mathlib.MeasureTheory.PiSystem
 
 /-!
 # Compact systems.
@@ -173,3 +172,5 @@ theorem _of_isCompact_of_T2Space [T2Space α] :
 end ClosedCompact
 
 end IsCompactSystem
+
+#min_imports

From 0983f2f202826e511fdbf3906d81f7ffd7e04d7c Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Fri, 2 May 2025 11:29:14 +0200
Subject: [PATCH 25/53] deleted hash

---
 Mathlib/Topology/Compactness/CompactSystem.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 7f458db4e0d27b..0ba8611fb79352 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -172,5 +172,3 @@ theorem _of_isCompact_of_T2Space [T2Space α] :
 end ClosedCompact
 
 end IsCompactSystem
-
-#min_imports

From eb4e37c6c299be30ffe71cf7af1f3deb4cbd7fde Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Thu, 22 May 2025 14:25:41 +0200
Subject: [PATCH 26/53] cs0

---
 Mathlib/Data/Set/Accumulate.lean              |   6 +-
 Mathlib/Data/Set/Dissipate.lean               |  85 +++---
 .../Topology/Compactness/CompactSystem.lean   | 271 +++++++++++++++---
 3 files changed, 280 insertions(+), 82 deletions(-)

diff --git a/Mathlib/Data/Set/Accumulate.lean b/Mathlib/Data/Set/Accumulate.lean
index 64d874f0e99e64..731684192a4470 100644
--- a/Mathlib/Data/Set/Accumulate.lean
+++ b/Mathlib/Data/Set/Accumulate.lean
@@ -8,7 +8,11 @@ import Mathlib.Data.Set.Lattice
 /-!
 # Accumulate
 
-The function `Accumulate` takes a set `s` and returns `⋃ y ≤ x, s y`.
+The function `Accumulate` takes `s : α → Set β` with `LE α` and returns `⋃ y ≤ x, s y`.
+
+In large parts, this file is parallel to `Mathlib.Data.Set.Dissipate`, where
+`Dissipate s := ⋂ y ≤ x, s y` is defined.
+
 -/
 
 
diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean
index da1a03f4593fc5..d54b6af373c2be 100644
--- a/Mathlib/Data/Set/Dissipate.lean
+++ b/Mathlib/Data/Set/Dissipate.lean
@@ -5,13 +5,20 @@ Authors: Peter Pfaffelhuber
 -/
 import Mathlib.Data.Set.Lattice
 import Mathlib.Order.Directed
+import Mathlib.MeasureTheory.PiSystem
 
 /-!
 # Dissipate
 
-The function `Dissipate` takes a set `s` and returns `⋂ y ≤ x, s y`.
+The function `Dissipate` takes `s : α → Set β` with `LE α` and returns `⋂ y ≤ x, s y`.
+
+In large parts, this file is parallel to `Mathlib.Data.Set.Accumulate`, where
+`Accumulate s := ⋃ y ≤ x, s y` is defined.
+
 -/
 
+open Nat
+
 variable {α β : Type*} {s : α → Set β}
 
 namespace Set
@@ -30,7 +37,7 @@ theorem dissipate_eq {s : ℕ → Set β} {n : ℕ} : Dissipate s n = ⋂ k < n
 theorem mem_dissipate [LE α] {x : α} {z : β} : z ∈ Dissipate s x ↔ ∀ y ≤ x, z ∈ s y := by
   simp only [dissipate_def, mem_iInter]
 
-theorem dissipate_subset [Preorder α] {x y : α} (hy : y ≤ x): Dissipate s x ⊆ s y :=
+theorem dissipate_subset [Preorder α] {x y : α} (hy : y ≤ x) : Dissipate s x ⊆ s y :=
   biInter_subset_of_mem hy
 
 theorem dissipate_subset_iInter [Preorder α] (x : α) : ⋂ i, s i ⊆ Dissipate s x := by
@@ -45,20 +52,23 @@ theorem dissipate_subset_dissipate [Preorder α] {x y} (h : y ≤ x) :
     Dissipate s x ⊆ Dissipate s y :=
   antitone_dissipate h
 
+@[simp]
 theorem biInter_dissipate [Preorder α] {s : α → Set β} {x : α} :
-    ⋂ y ≤ x, s y = ⋂ y ≤ x, ⋂ z ≤ y, s z := by
+    ⋂ y ≤ x, Dissipate s y = Dissipate s x := by
   apply Subset.antisymm
-  · simp only [subset_iInter_iff, Dissipate]
-    exact fun i hi z hz ↦ biInter_subset_of_mem <| le_trans hz hi
   · apply iInter_mono fun z y hy ↦ ?_
-    simp only [mem_iInter] at *
+    simp only [dissipate_def, mem_iInter] at *
     exact fun h ↦ hy h z <| le_refl z
+  · simp only [subset_iInter_iff, Dissipate]
+    exact fun i hi z hz ↦ biInter_subset_of_mem <| le_trans hz hi
 
-theorem iInter_dissipate [Preorder α] : ⋂ x, s x = ⋂ x, Dissipate s x := by
+@[simp]
+theorem iInter_dissipate [Preorder α] : ⋂ x, Dissipate s x = ⋂ x, s x := by
   apply Subset.antisymm <;> simp_rw [subset_def, mem_iInter, mem_dissipate]
-  · exact fun z h x' y hy ↦ h y
   · exact fun z h x' ↦ h x' x' (le_refl x')
+  · exact fun z h x' y hy ↦ h y
 
+@[simp]
 lemma dissipate_bot [PartialOrder α] [OrderBot α] (s : α → Set β) : Dissipate s ⊥ = s ⊥ := by
   simp only [dissipate_def, le_bot_iff, iInter_iInter_eq_left]
 
@@ -66,7 +76,7 @@ open Nat
 
 @[simp]
 theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) :
-    ⋂ y, ⋂ (_ : y ≤ n + 1), s y = Dissipate s n ∩ s (n + 1) := by
+    Dissipate s (n + 1) = Dissipate s n ∩ s (n + 1) := by
   ext x
   refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
   · simp only [mem_inter_iff, mem_iInter, Dissipate] at *
@@ -79,11 +89,12 @@ theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) :
     · simp only [not_le] at h
       exact le_antisymm hi h ▸ hx.2
 
+@[simp]
 lemma dissipate_zero (s : ℕ → Set β) : Dissipate s 0 = s 0 := by
   simp [dissipate_def]
 
-lemma subset_of_directed {s : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) s)
-    (n : ℕ) : ∃ m, ⋂ i ≤ n, s i ⊇ s m := by
+lemma exists_subset_dissipate_of_directed {s : ℕ → Set α}
+  (hd : Directed (fun (x1 x2 : Set α) => x2 ⊆ x1) s) (n : ℕ) : ∃ m, s m ⊆ Dissipate s n := by
   induction n with
   | zero => use 0; simp
   | succ n hn =>
@@ -95,62 +106,52 @@ lemma subset_of_directed {s : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set 
     simp only [subset_inter_iff]
     exact ⟨le_trans hk.1 hm, hk.2⟩
 
-lemma empty_of_directed {s : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) s) :
-      (∃ n, s n = ∅) ↔ (∃ n, Dissipate s n = ∅) := by
-  refine ⟨fun ⟨n, hn⟩ ↦ ⟨n, ?_⟩, ?_⟩
-  · by_cases hn' : n = 0
-    · rw [hn']
-      exact Eq.trans (dissipate_zero s) (hn' ▸ hn)
-    · obtain ⟨k, hk⟩ := exists_eq_succ_of_ne_zero hn'
-      rw [hk, dissipate_def, dissipate_succ, ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
+lemma exists_dissipate_eq_empty_iff {s : ℕ → Set α}
+    (hd : Directed (fun (x1 x2 : Set α) => x2 ⊆ x1) s) :
+      (∃ n, Dissipate s n = ∅) ↔ (∃ n, s n = ∅) := by
+  refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n, ?_⟩⟩
   · rw [← not_imp_not]
     push_neg
     intro h n
-    obtain ⟨m, hm⟩ := subset_of_directed hd n
+    obtain ⟨m, hm⟩ := exists_subset_dissipate_of_directed hd n
     exact Set.Nonempty.mono hm (h m)
+  · by_cases hn' : n = 0
+    · rw [hn']
+      exact Eq.trans (dissipate_zero s) (hn' ▸ hn)
+    · obtain ⟨k, hk⟩ := exists_eq_add_one_of_ne_zero hn'
+      rw [hk, dissipate_succ, ← hk, hn, Set.inter_empty]
 
-lemma dissipate_directed {s : ℕ → Set α} :
-    Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) (Dissipate s) :=
+lemma directed_dissipate {s : ℕ → Set α} :
+    Directed (fun (x1 x2 : Set α) => x2 ⊆ x1) (Dissipate s) :=
      antitone_dissipate.directed_ge
 
-lemma mem_subset_dissipate_of_directed (C : ℕ → Set α)
-    (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) (n : ℕ) : ∃ m, Dissipate C n ⊇ C m := by
-  induction n with
-  | zero => use 0; simp
-  | succ n hn =>
-    obtain ⟨m, hm⟩ := hn
-    obtain ⟨k, hk⟩ := hd m (n+1)
-    simp_rw [dissipate_def, dissipate_succ]
-    simp at hk
-    exact ⟨k, Set.subset_inter_iff.mpr <| ⟨le_trans hk.1 hm, hk.2⟩⟩
-
-lemma dissipate_exists_empty_iff_of_directed (C : ℕ → Set α)
-    (hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C) :
-      (∃ n, C n = ∅) ↔ (∃ n, Dissipate C n = ∅) := by
+lemma exists_dissipate_eq_empty_iff_of_directed (C : ℕ → Set α)
+    (hd : Directed (fun (x1 x2 : Set α) => x2 ⊆ x1) C) :
+    (∃ n, C n = ∅) ↔ (∃ n, Dissipate C n = ∅) := by
   refine ⟨fun ⟨n, hn⟩ ↦ ⟨n, ?_⟩ , ?_⟩
   · by_cases hn' : n = 0
     · rw [hn', dissipate_zero]
       exact hn' ▸ hn
     · obtain ⟨k, hk⟩ := exists_eq_succ_of_ne_zero hn'
-      simp_rw [hk, succ_eq_add_one, dissipate_def, dissipate_succ,
+      simp_rw [hk, succ_eq_add_one, dissipate_succ,
         ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
   · rw [← not_imp_not]
     push_neg
     intro h n
-    obtain ⟨m, hm⟩ := mem_subset_dissipate_of_directed C hd n
+    obtain ⟨m, hm⟩ := exists_subset_dissipate_of_directed hd n
     exact Set.Nonempty.mono hm (h m)
 
 /-- For a ∩-stable attribute `p` on `Set α` and a sequence of sets `s` with this attribute,
-`p ⋂ i ≤ n, s n` holds. -/
+`p (Dissipate s n)` holds. -/
 lemma dissipate_of_piSystem {s : ℕ → Set α} {p : Set α → Prop}
-    (hp : ∀ (s t : Set α), p s → p t → p (s ∩ t)) (h : ∀ n, p (s n)) (n : ℕ) :
+    (hp : IsPiSystem p) (h : ∀ n, p (s n)) (n : ℕ) (h' : (Dissipate s n).Nonempty) :
       p (Dissipate s n) := by
   induction n with
   | zero =>
     simp only [dissipate_def, le_zero_eq, iInter_iInter_eq_left]
     exact h 0
   | succ n hn =>
-    rw [dissipate_def, dissipate_succ]
-    exact hp (Dissipate s n) (s (n+1)) hn (h (n+1))
+    rw [dissipate_succ] at *
+    apply hp (Dissipate s n) (hn (Nonempty.left h')) (s (n+1)) (h (n+1)) h'
 
 end Set
diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 0ba8611fb79352..2fec7c63cf984f 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -38,19 +38,21 @@ end definition
 
 namespace IsCompactSystem
 
-/-- In a compact system, given a countable family with empty intersection, we choose a finite
-subfamily with empty intersection. -/
+open Classical in
+/-- In a compact system, given a countable family with `⋂ i, C i = ∅`, we choose the smallest `n`
+with `⋂ (i ≤ n), C i = ∅`. -/
 noncomputable
-def max_of_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i))
+def finite_of_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i))
     (hC_empty : ⋂ i, C i = ∅) : ℕ :=
-  (hp C hC hC_empty).choose
+  Nat.find (hp C hC hC_empty)
 
-lemma iInter_eq_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i))
+open Classical in
+lemma dissipate_eq_empty (hp : IsCompactSystem p) (hC : ∀ i, p (C i))
     (hC_empty : ⋂ i, C i = ∅) :
-    Dissipate C (hp.max_of_empty hC hC_empty) = ∅ :=
-  (hp C hC hC_empty).choose_spec
+    Dissipate C (hp.finite_of_empty hC hC_empty) = ∅ := by
+  apply Nat.find_spec (hp C hC hC_empty)
 
-theorem iff_of_nempty (p : Set α → Prop) :
+theorem iff_nonempty_iInter (p : Set α → Prop) :
     IsCompactSystem p ↔ (∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ (n : ℕ),
       (Dissipate C n).Nonempty) → (⋂ i, C i).Nonempty) := by
   refine ⟨fun h C hC hn ↦ ?_, fun h C hC ↦ ?_⟩ <;> have h2 := not_imp_not.mpr <| h C hC
@@ -61,9 +63,9 @@ theorem iff_of_nempty (p : Set α → Prop) :
 
 /-- In this equivalent formulation for a compact system,
 note that we use `⋂ k < n, C k` rather than `⋂ k ≤ n, C k`. -/
-lemma iff_of_not_empty (p : Set α → Prop) : IsCompactSystem p ↔
-    ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, ⋂ k < n, C k ≠ ∅) → ⋂ i, C i ≠ ∅ := by
-  simp_rw [← Set.nonempty_iff_ne_empty, iff_of_nempty]
+lemma iff_nonempty_iInter_of_lt (p : Set α → Prop) : IsCompactSystem p ↔
+    ∀ C : ℕ → Set α, (∀ i, p (C i)) → (∀ n, (⋂ k < n, C k).Nonempty) → (⋂ i, C i).Nonempty := by
+  simp_rw [iff_nonempty_iInter]
   refine ⟨fun h C hi h'↦ ?_, fun h C hi h' ↦ ?_⟩
   · apply h C hi
     exact fun n ↦ dissipate_eq ▸ (h' (n + 1))
@@ -78,18 +80,177 @@ lemma iff_of_not_empty (p : Set α → Prop) : IsCompactSystem p ↔
     rw [mem_iInter₂, mem_iInter₂]
     exact fun h i hi ↦ h i hi.le
 
-theorem iff_directed (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
-    (IsCompactSystem p) ↔
-    (∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
-      ⋂ i, C i = ∅ → ∃ (n : ℕ), C n = ∅) := by
+/-- 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
+
+/-- A set system is a compact system iff adding `∅` gives a compact system. -/
+lemma iff_isCompactSystem_of_or_empty : IsCompactSystem p ↔
+    IsCompactSystem (fun s ↦ (p s ∨ (s = ∅))) := by
+  refine ⟨fun h s h' hd ↦ ?_, fun h ↦ mono h (fun s ↦ fun a ↦ Or.symm (Or.inr a))⟩
+  by_cases g : ∃ n, s n = ∅
+  · use g.choose
+    rw [← subset_empty_iff] at hd ⊢
+    exact le_trans (dissipate_subset (by rfl)) g.choose_spec.le
+  · push_neg at g
+    have hj (i : _) : p (s i) := by
+      rcases h' i with a | b
+      · exact a
+      · exfalso
+        revert g i
+        simp_rw [← Set.not_nonempty_iff_eq_empty]
+        simp_rw [imp_false, not_not]
+        exact fun h i ↦ h i
+    exact h s hj hd
+
+lemma of_IsEmpty (h : IsEmpty α) (p : Set α → Prop) : IsCompactSystem p :=
+  fun s _ _ ↦ ⟨0, Set.eq_empty_of_isEmpty (Dissipate s 0)⟩
+
+/-- A set system is a compact system iff adding `univ` gives a compact system. -/
+lemma iff_isCompactSystem_of_or_univ : IsCompactSystem p ↔
+    IsCompactSystem (fun s ↦ (p s ∨ (s = univ))) := by
+  refine ⟨fun h ↦ ?_, fun h ↦ mono h (fun s ↦ fun a ↦ Or.symm (Or.inr a))⟩
+  wlog ht : Nonempty α
+  · rw [not_nonempty_iff] at ht
+    apply of_IsEmpty ht
+  · rw [iff_nonempty_iInter] at h ⊢
+    intro s h' hd
+    classical
+    by_cases h₀ : ∀ n, ¬p (s n)
+    · have h₁ : ∀ n, s n = univ := by
+        intro n
+        simp only [h₀, false_or] at h'
+        exact h' n
+      simp_rw [h₁, iInter_univ, Set.univ_nonempty]
+    · push_neg at h₀
+      let n := Nat.find h₀
+      let s' := fun i ↦ if p (s i) then s i else s n
+      have h₁ : ∀ i, p (s' i) := by
+        intro i
+        by_cases h₁ : p (s i)
+        · have h₂ : s' i = s i := if_pos h₁
+          exact h₂ ▸ h₁
+        · have h₂ : s' i = s n := if_neg h₁
+          exact h₂ ▸ (Nat.find_spec h₀)
+      have h₃ : ∀ i, (p (s i) → s' i = s i) := fun i h ↦ if_pos h
+      have h₄ : ∀ i, (¬p (s i) → s' i = s n) := fun i h ↦ if_neg h
+      have h₂ : ⋂ i, s i = ⋂ i, s' i := by
+        ext x
+        simp only [mem_iInter]
+        refine ⟨fun h i ↦ ?_, fun h i ↦ ?_⟩
+        · by_cases h₅ : p (s i)
+          · exact (h₃ i h₅) ▸ h i
+          · exact (h₄ i h₅) ▸ h n
+        · have h₄ : s i = s' i ∨ s i = univ := by
+            rcases h' i with a | b
+            · exact Or.inl <| Eq.symm (if_pos a)
+            · exact Or.inr b
+          rcases h₄ with a | b
+          · exact a ▸ h i
+          · simp [b]
+      apply h₂ ▸ h s' h₁
+      by_contra! a
+      obtain ⟨j, hj⟩ := a
+      have h₂ : ∀ (v : ℕ) (hv : n ≤ v), Dissipate s v = Dissipate s' v:= by
+        intro v hv
+        ext x
+        refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ <;> simp only [dissipate_def, mem_iInter] at h ⊢ <;>
+          intro i hi
+        · by_cases h₅ : p (s i)
+          · exact (h₃ i h₅) ▸ h i hi
+          · exact (h₄ i h₅) ▸ h n hv
+        · by_cases h₅ : p (s i)
+          · exact (h₃ i h₅) ▸ h i hi
+          · have h₆ : s i = univ := by
+              specialize h' i
+              simp only [h₅, false_or] at h'
+              exact h'
+            simp only [h₆, Set.mem_univ]
+      have h₇ : Dissipate s' (max j n) = ∅ := by
+        rw [← subset_empty_iff] at hj ⊢
+        exact le_trans (antitone_dissipate (Nat.le_max_left j n)) hj
+      specialize h₂ (max j n) (Nat.le_max_right j n)
+      specialize hd (max j n)
+      rw [h₂, Set.nonempty_iff_ne_empty, h₇] at hd
+      exact hd rfl
+
+example (a b : Set α) (ha : a = ∅ ) : a ∩ b = ∅ := by
+  subst ha
+  simp_all only [Set.empty_inter]
+
+example (P Q : Prop) (hP : ¬P) (hPQ : P ∨ Q) : Q := by
+  simp_all only [false_or]
+
+
+theorem isPiSystem.iff_isPiSystem_or_empty : IsPiSystem p ↔ IsPiSystem (fun s ↦ p s ∨ s = ∅) := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · intro a ha b hb hab
+    rcases ha with ha₁ | ha₂
+    · rcases hb with hb₁ | hb₂
+      · left
+        exact hpi a ha₁ b hb₁ hab
+      · right
+        exact hb₂ ▸ (Set.inter_empty a)
+    · simp only [ha₂, Set.empty_inter]
+      right
+      rfl
+  · intro a ha b hb hab
+    simp [IsPiSystem] at h
+    specialize h a
+    by_cases ha : a = ∅
+    · sorry
+    ·
+    specialize h a (Or.inl ha) b (Or.inl hb) hab
+    by_cases ha : a = ∅
+    · sorry
+    ·
+    apply h a ha b hb hab
+    sorry
+
+theorem iff_directed (hpi : IsPiSystem p) :
+    IsCompactSystem p ↔
+    ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
+      ⋂ i, C i = ∅ → ∃ (n : ℕ), C n = ∅ := by
+  rw [iff_isCompactSystem_of_or_empty]
   refine ⟨fun h ↦ fun C hdi hi ↦ ?_, fun h C h1 h2 ↦ ?_⟩
-  · rw [dissipate_exists_empty_iff_of_directed C hdi]
-    exact h C hi
-  · rw [← biInter_le_eq_iInter] at h2
-    exact h (Dissipate C) dissipate_directed (dissipate_of_piSystem hpi h1) h2
+  · rw [exists_dissipate_eq_empty_iff_of_directed C hdi]
+    apply h C
+    exact fun i ↦ Or.inl (hi i)
+  · have hpi' : IsPiSystem (fun s ↦ p s ∨ s = ∅) := by
+      intro a ha b hb hab
+      rcases ha with ha₁ | ha₂
+      · rcases hb with hb₁ | hb₂
+        · left
+          exact hpi a ha₁ b hb₁ hab
+        · right
+          exact hb₂ ▸ (Set.inter_empty a)
+      · simp only [ha₂, Set.empty_inter]
+        right
+        rfl
+    rw [← biInter_le_eq_iInter] at h2
+    obtain h' := h (Dissipate C) directed_dissipate
+    have h₀ : (∀ (n : ℕ), p (Dissipate C n) ∨ Dissipate C n = ∅) → ⋂ n, Dissipate C n = ∅ →
+      ∃ n, Dissipate C n = ∅ := by
+      intro h₀ h₁
+      by_cases f : ∀ n, p (Dissipate C n)
+      · apply h' f h₁
+      · push_neg at f
+        obtain ⟨n, hn⟩ := f
+        use n
+        specialize h₀ n
+        simp_all only [false_or]
+    obtain h'' := dissipate_of_piSystem hpi' h1
+    have h₁ :  ∀ (n : ℕ), p (Dissipate C n) ∨ Dissipate C n = ∅ := by
+      intro n
+      by_cases g : (Dissipate C n).Nonempty
+      · exact h'' n g
+      · right
+        exact Set.not_nonempty_iff_eq_empty.mp g
+    apply h₀ h₁ h2
+
 
-theorem iff_directed' (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
-    (IsCompactSystem p) ↔
+theorem iff_directed' (hpi : IsPiSystem p) :
+    IsCompactSystem p ↔
     ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
     (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty  := by
   rw [IsCompactSystem.iff_directed hpi]
@@ -97,16 +258,52 @@ theorem iff_directed' (hpi : ∀ (s t : Set α), p s → p t → p (s ∩ t)) :
   · exact h1 C h3 h4
   · exact h1 C h3 s
 
-/-- Any subset of a compact system is a compact system. -/
-theorem of_supset {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
-
-section ClosedCompact
+section IsCompactIsClosed
 
 variable (α : Type*) [TopologicalSpace α]
 
+/-- The set of compact and closed sets is a compact system. -/
+theorem of_isCompact_isClosed :
+    IsCompactSystem (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by
+  let p := fun (s : Set α) ↦ IsCompact s ∧ IsClosed s
+  have h2 : IsPiSystem p := by
+    intro s hs t ht _
+    refine ⟨IsCompact.inter_left ht.1 hs.2, IsClosed.inter hs.2 ht.2⟩
+  rw [IsCompactSystem.iff_directed' h2]
+  intro s hs h1 h2
+  let s' := fun (i : { j : ℕ | s j ≠ univ}) ↦ s i
+  have hs' : Directed (fun x1 x2 ↦ x1 ⊇ x2) s' := by
+    intro a b
+    obtain ⟨z, hz1, hz2⟩ := hs a.val b.val
+    have hz : s z ≠ univ := fun h ↦ a.prop <| eq_univ_of_subset hz1 h
+    use ⟨z, hz⟩
+  have htcl : ∀ (i : { j : ℕ | s j ≠ univ}), IsClosed (s i) :=
+    fun i ↦ (Or.resolve_right (h1 i.val) i.prop).2
+  have htco : ∀ (i : { j : ℕ | s j ≠ univ}), IsCompact (s i) :=
+    fun i ↦ (Or.resolve_right (h1 i.val) i.prop).1
+  haveI f : Nonempty α := by
+    apply nonempty_of_exists _
+    · exact fun x ↦ x ∈ s 0
+    · exact h2 0
+  by_cases h : Nonempty ↑{j | s j ≠ Set.univ}
+  · have g :  (⋂ i, s' i).Nonempty → (⋂ i, s i).Nonempty := by
+      rw [Set.nonempty_iInter, Set.nonempty_iInter]
+      rintro ⟨x, hx⟩
+      use x
+      intro i
+      by_cases g : s i ≠ univ
+      · exact hx ⟨i, g⟩
+      · simp only [ne_eq, not_not, s'] at g
+        rw [g]
+        simp only [Set.mem_univ]
+    apply g <| IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed s' hs'
+      (fun j ↦ h2 j) htco htcl
+  · simp only [ne_eq, coe_setOf, nonempty_subtype, not_exists, not_not, s'] at h
+    simp [s', h]
+
+
 /-- The set of sets which are either compact and closed, or `univ`, is a compact system. -/
-theorem isClosedCompactOrUnivs :
+theorem of_isCompact_isClosed_or_univ :
     IsCompactSystem (fun s : Set α ↦ (IsCompact s ∧ IsClosed s) ∨ (s = univ)) := by
   let p := fun (s : Set α) ↦ (IsCompact s ∧ IsClosed s) ∨ (s = univ)
   have h2 : ∀ (s t : Set α), p s → p t → p (s ∩ t) := by
@@ -150,25 +347,21 @@ theorem isClosedCompactOrUnivs :
     apply g <| IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed s' hs'
       (fun j ↦ h2 j) htco htcl
   · simp only [ne_eq, coe_setOf, nonempty_subtype, not_exists, not_not, s'] at h
-    simp only [nonempty_iInter, s', h]
-    simp only [Set.mem_univ, implies_true, exists_const, s']
+    simp [s', h]
 
 /-- The set of compact and closed sets is a compact system. -/
-theorem isClosedCompacts :
+theorem of_isCompact_isClosed :
     IsCompactSystem (fun s : Set α ↦ IsCompact s ∧ IsClosed s) :=
-  IsCompactSystem.of_supset (isClosedCompactOrUnivs α) (fun _ hs ↦ Or.inl hs)
+  IsCompactSystem.mono (of_isCompact_isClosed_or_univ α) (fun _ hs ↦ Or.inl hs)
 
-theorem isCompacts (h : ∀ {s : Set α}, IsCompact s → IsClosed s) :
+/-- In a `T2Space` the set of compact sets is a compact system. -/
+theorem of_isCompact [T2Space α] :
     IsCompactSystem (fun s : Set α ↦ IsCompact s) := by
   have h : (fun s : Set α ↦ IsCompact s) = (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by
     ext s
-    refine ⟨fun h' ↦ ⟨h', h h'⟩, fun h' ↦ h'.1⟩
-  exact h ▸ (isClosedCompacts α)
-
-/-- In a `T2Space` The set of compact sets is a compact system. -/
-theorem _of_isCompact_of_T2Space [T2Space α] :
-    IsCompactSystem (fun s : Set α ↦ IsCompact s) := (isCompacts α) (fun hs ↦ hs.isClosed)
+    refine ⟨fun h' ↦ ⟨h', h'.isClosed⟩, fun h ↦ h.1⟩
+  exact h ▸ (of_isCompact_isClosed α)
 
-end ClosedCompact
+end IsCompactIsClosed
 
 end IsCompactSystem

From 2125c0263267725bdc31701da2bb5276763070d9 Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Fri, 23 May 2025 23:50:20 +0200
Subject: [PATCH 27/53] fininsh?

---
 .../Topology/Compactness/CompactSystem.lean   | 131 +++---------------
 1 file changed, 22 insertions(+), 109 deletions(-)

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 2fec7c63cf984f..17c4fc989626ce 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -18,6 +18,8 @@ This files defines compact systems of sets.
 
 ## Main results
 
+* `IsCompactSystemiff_isCompactSystem_of_or_univ`: A set system is a compact
+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`.
@@ -108,7 +110,7 @@ lemma of_IsEmpty (h : IsEmpty α) (p : Set α → Prop) : IsCompactSystem p :=
 
 /-- A set system is a compact system iff adding `univ` gives a compact system. -/
 lemma iff_isCompactSystem_of_or_univ : IsCompactSystem p ↔
-    IsCompactSystem (fun s ↦ (p s ∨ (s = univ))) := by
+    IsCompactSystem (fun s ↦ (p s ∨ s = univ)) := by
   refine ⟨fun h ↦ ?_, fun h ↦ mono h (fun s ↦ fun a ↦ Or.symm (Or.inr a))⟩
   wlog ht : Nonempty α
   · rw [not_nonempty_iff] at ht
@@ -117,42 +119,34 @@ lemma iff_isCompactSystem_of_or_univ : IsCompactSystem p ↔
     intro s h' hd
     classical
     by_cases h₀ : ∀ n, ¬p (s n)
-    · have h₁ : ∀ n, s n = univ := by
-        intro n
-        simp only [h₀, false_or] at h'
-        exact h' n
-      simp_rw [h₁, iInter_univ, Set.univ_nonempty]
+    · simp only [h₀, false_or] at h'
+      simp_rw [h', iInter_univ, Set.univ_nonempty]
     · push_neg at h₀
       let n := Nat.find h₀
       let s' := fun i ↦ if p (s i) then s i else s n
       have h₁ : ∀ i, p (s' i) := by
         intro i
         by_cases h₁ : p (s i)
-        · have h₂ : s' i = s i := if_pos h₁
-          exact h₂ ▸ h₁
-        · have h₂ : s' i = s n := if_neg h₁
-          exact h₂ ▸ (Nat.find_spec h₀)
+        · simp only [h₁, ↓reduceIte, s']
+        · simp only [h₁, ↓reduceIte, Nat.find_spec h₀, s', n]
       have h₃ : ∀ i, (p (s i) → s' i = s i) := fun i h ↦ if_pos h
       have h₄ : ∀ i, (¬p (s i) → s' i = s n) := fun i h ↦ if_neg h
       have h₂ : ⋂ i, s i = ⋂ i, s' i := by
+        simp only [s'] at *
         ext x
         simp only [mem_iInter]
         refine ⟨fun h i ↦ ?_, fun h i ↦ ?_⟩
-        · by_cases h₅ : p (s i)
-          · exact (h₃ i h₅) ▸ h i
-          · exact (h₄ i h₅) ▸ h n
-        · have h₄ : s i = s' i ∨ s i = univ := by
-            rcases h' i with a | b
-            · exact Or.inl <| Eq.symm (if_pos a)
-            · exact Or.inr b
-          rcases h₄ with a | b
-          · exact a ▸ h i
-          · simp [b]
+        · by_cases h' : p (s i) <;> simp only [h', ↓reduceIte, h, s', n]
+        · specialize h' i
+          specialize h i
+          rcases h' with a | b
+          · simp only [a, ↓reduceIte, s', n] at h
+            exact h
+          · simp only [b, Set.mem_univ]
       apply h₂ ▸ h s' h₁
       by_contra! a
       obtain ⟨j, hj⟩ := a
-      have h₂ : ∀ (v : ℕ) (hv : n ≤ v), Dissipate s v = Dissipate s' v:= by
-        intro v hv
+      have h₂ (v : ℕ) (hv : n ≤ v) : Dissipate s v = Dissipate s' v:= by
         ext x
         refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ <;> simp only [dissipate_def, mem_iInter] at h ⊢ <;>
           intro i hi
@@ -174,39 +168,6 @@ lemma iff_isCompactSystem_of_or_univ : IsCompactSystem p ↔
       rw [h₂, Set.nonempty_iff_ne_empty, h₇] at hd
       exact hd rfl
 
-example (a b : Set α) (ha : a = ∅ ) : a ∩ b = ∅ := by
-  subst ha
-  simp_all only [Set.empty_inter]
-
-example (P Q : Prop) (hP : ¬P) (hPQ : P ∨ Q) : Q := by
-  simp_all only [false_or]
-
-
-theorem isPiSystem.iff_isPiSystem_or_empty : IsPiSystem p ↔ IsPiSystem (fun s ↦ p s ∨ s = ∅) := by
-  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-  · intro a ha b hb hab
-    rcases ha with ha₁ | ha₂
-    · rcases hb with hb₁ | hb₂
-      · left
-        exact hpi a ha₁ b hb₁ hab
-      · right
-        exact hb₂ ▸ (Set.inter_empty a)
-    · simp only [ha₂, Set.empty_inter]
-      right
-      rfl
-  · intro a ha b hb hab
-    simp [IsPiSystem] at h
-    specialize h a
-    by_cases ha : a = ∅
-    · sorry
-    ·
-    specialize h a (Or.inl ha) b (Or.inl hb) hab
-    by_cases ha : a = ∅
-    · sorry
-    ·
-    apply h a ha b hb hab
-    sorry
-
 theorem iff_directed (hpi : IsPiSystem p) :
     IsCompactSystem p ↔
     ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
@@ -248,7 +209,6 @@ theorem iff_directed (hpi : IsPiSystem p) :
         exact Set.not_nonempty_iff_eq_empty.mp g
     apply h₀ h₁ h2
 
-
 theorem iff_directed' (hpi : IsPiSystem p) :
     IsCompactSystem p ↔
     ∀ (C : ℕ → Set α), ∀ (_ : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) C), (∀ i, p (C i)) →
@@ -260,7 +220,7 @@ theorem iff_directed' (hpi : IsPiSystem p) :
 
 section IsCompactIsClosed
 
-variable (α : Type*) [TopologicalSpace α]
+variable {α : Type*} [TopologicalSpace α]
 
 /-- The set of compact and closed sets is a compact system. -/
 theorem of_isCompact_isClosed :
@@ -278,9 +238,9 @@ theorem of_isCompact_isClosed :
     have hz : s z ≠ univ := fun h ↦ a.prop <| eq_univ_of_subset hz1 h
     use ⟨z, hz⟩
   have htcl : ∀ (i : { j : ℕ | s j ≠ univ}), IsClosed (s i) :=
-    fun i ↦ (Or.resolve_right (h1 i.val) i.prop).2
+    fun i ↦ (h1 i).2
   have htco : ∀ (i : { j : ℕ | s j ≠ univ}), IsCompact (s i) :=
-    fun i ↦ (Or.resolve_right (h1 i.val) i.prop).1
+    fun i ↦ (h1 i).1
   haveI f : Nonempty α := by
     apply nonempty_of_exists _
     · exact fun x ↦ x ∈ s 0
@@ -301,58 +261,11 @@ theorem of_isCompact_isClosed :
   · simp only [ne_eq, coe_setOf, nonempty_subtype, not_exists, not_not, s'] at h
     simp [s', h]
 
-
 /-- The set of sets which are either compact and closed, or `univ`, is a compact system. -/
 theorem of_isCompact_isClosed_or_univ :
     IsCompactSystem (fun s : Set α ↦ (IsCompact s ∧ IsClosed s) ∨ (s = univ)) := by
-  let p := fun (s : Set α) ↦ (IsCompact s ∧ IsClosed s) ∨ (s = univ)
-  have h2 : ∀ (s t : Set α), p s → p t → p (s ∩ t) := by
-    intro s t hs ht
-    by_cases hs' : s = univ
-    · rw [hs', univ_inter]
-      exact ht
-    · by_cases ht' : t = univ
-      · rw [ht', inter_comm, univ_inter]
-        exact hs
-      · exact Or.inl <| ⟨IsCompact.inter_right (Or.resolve_right hs hs').1
-        (Or.resolve_right ht ht').2, IsClosed.inter (Or.resolve_right hs hs').2
-          (Or.resolve_right ht ht').2⟩
-  rw [IsCompactSystem.iff_directed' h2]
-  intro s hs h1 h2
-  let s' := fun (i : { j : ℕ | s j ≠ univ}) ↦ s i
-  have hs' : Directed (fun x1 x2 ↦ x1 ⊇ x2) s' := by
-    intro a b
-    obtain ⟨z, hz1, hz2⟩ := hs a.val b.val
-    have hz : s z ≠ univ := fun h ↦ a.prop <| eq_univ_of_subset hz1 h
-    use ⟨z, hz⟩
-  have htcl : ∀ (i : { j : ℕ | s j ≠ univ}), IsClosed (s i) :=
-    fun i ↦ (Or.resolve_right (h1 i.val) i.prop).2
-  have htco : ∀ (i : { j : ℕ | s j ≠ univ}), IsCompact (s i) :=
-    fun i ↦ (Or.resolve_right (h1 i.val) i.prop).1
-  haveI f : Nonempty α := by
-    apply nonempty_of_exists _
-    · exact fun x ↦ x ∈ s 0
-    · exact h2 0
-  by_cases h : Nonempty ↑{j | s j ≠ Set.univ}
-  · have g :  (⋂ i, s' i).Nonempty → (⋂ i, s i).Nonempty := by
-      rw [Set.nonempty_iInter, Set.nonempty_iInter]
-      rintro ⟨x, hx⟩
-      use x
-      intro i
-      by_cases g : s i ≠ univ
-      · exact hx ⟨i, g⟩
-      · simp only [ne_eq, not_not, s'] at g
-        rw [g]
-        simp only [Set.mem_univ]
-    apply g <| IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed s' hs'
-      (fun j ↦ h2 j) htco htcl
-  · simp only [ne_eq, coe_setOf, nonempty_subtype, not_exists, not_not, s'] at h
-    simp [s', h]
-
-/-- The set of compact and closed sets is a compact system. -/
-theorem of_isCompact_isClosed :
-    IsCompactSystem (fun s : Set α ↦ IsCompact s ∧ IsClosed s) :=
-  IsCompactSystem.mono (of_isCompact_isClosed_or_univ α) (fun _ hs ↦ Or.inl hs)
+  rw [← iff_isCompactSystem_of_or_univ]
+  exact of_isCompact_isClosed
 
 /-- In a `T2Space` the set of compact sets is a compact system. -/
 theorem of_isCompact [T2Space α] :
@@ -360,7 +273,7 @@ theorem of_isCompact [T2Space α] :
   have h : (fun s : Set α ↦ IsCompact s) = (fun s : Set α ↦ IsCompact s ∧ IsClosed s) := by
     ext s
     refine ⟨fun h' ↦ ⟨h', h'.isClosed⟩, fun h ↦ h.1⟩
-  exact h ▸ (of_isCompact_isClosed α)
+  exact h ▸ (of_isCompact_isClosed)
 
 end IsCompactIsClosed
 

From 285a883d9d5f49db780067e14ae19d3cd332490f Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Fri, 30 May 2025 11:34:53 +0200
Subject: [PATCH 28/53] repair dissipate

---
 Mathlib/Data/Set/Dissipate.lean | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Data/Set/Dissipate.lean b/Mathlib/Data/Set/Dissipate.lean
index d54b6af373c2be..c4c92267e75a92 100644
--- a/Mathlib/Data/Set/Dissipate.lean
+++ b/Mathlib/Data/Set/Dissipate.lean
@@ -54,7 +54,7 @@ theorem dissipate_subset_dissipate [Preorder α] {x y} (h : y ≤ x) :
 
 @[simp]
 theorem biInter_dissipate [Preorder α] {s : α → Set β} {x : α} :
-    ⋂ y ≤ x, Dissipate s y = Dissipate s x := by
+    ⋂ y, ⋂ (_ : y ≤ x), ⋂ y_1, ⋂ (_ : y_1 ≤ y), s y_1 = ⋂ y, ⋂ (_ : y ≤ x), s y := by
   apply Subset.antisymm
   · apply iInter_mono fun z y hy ↦ ?_
     simp only [dissipate_def, mem_iInter] at *
@@ -63,12 +63,11 @@ theorem biInter_dissipate [Preorder α] {s : α → Set β} {x : α} :
     exact fun i hi z hz ↦ biInter_subset_of_mem <| le_trans hz hi
 
 @[simp]
-theorem iInter_dissipate [Preorder α] : ⋂ x, Dissipate s x = ⋂ x, s x := by
-  apply Subset.antisymm <;> simp_rw [subset_def, mem_iInter, mem_dissipate]
+theorem iInter_dissipate [Preorder α] : ⋂ x, ⋂ y, ⋂ (_ : y ≤ x), s y = ⋂ x, s x := by
+  apply Subset.antisymm <;> simp_rw [subset_def, mem_iInter]
   · exact fun z h x' ↦ h x' x' (le_refl x')
   · exact fun z h x' y hy ↦ h y
 
-@[simp]
 lemma dissipate_bot [PartialOrder α] [OrderBot α] (s : α → Set β) : Dissipate s ⊥ = s ⊥ := by
   simp only [dissipate_def, le_bot_iff, iInter_iInter_eq_left]
 
@@ -76,7 +75,8 @@ open Nat
 
 @[simp]
 theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) :
-    Dissipate s (n + 1) = Dissipate s n ∩ s (n + 1) := by
+    ⋂ y, ⋂ (_ : y ≤ n + 1), s y = (⋂ y, ⋂ (_ : y ≤ n), s y) ∩ s (n + 1)
+    := by
   ext x
   refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
   · simp only [mem_inter_iff, mem_iInter, Dissipate] at *
@@ -89,7 +89,6 @@ theorem dissipate_succ (s : ℕ → Set α) (n : ℕ) :
     · simp only [not_le] at h
       exact le_antisymm hi h ▸ hx.2
 
-@[simp]
 lemma dissipate_zero (s : ℕ → Set β) : Dissipate s 0 = s 0 := by
   simp [dissipate_def]
 
@@ -99,7 +98,7 @@ lemma exists_subset_dissipate_of_directed {s : ℕ → Set α}
   | zero => use 0; simp
   | succ n hn =>
     obtain ⟨m, hm⟩ := hn
-    simp_rw [dissipate_succ]
+    simp_rw [dissipate_def, dissipate_succ]
     obtain ⟨k, hk⟩ := hd m (n+1)
     simp at hk
     use k
@@ -119,7 +118,7 @@ lemma exists_dissipate_eq_empty_iff {s : ℕ → Set α}
     · rw [hn']
       exact Eq.trans (dissipate_zero s) (hn' ▸ hn)
     · obtain ⟨k, hk⟩ := exists_eq_add_one_of_ne_zero hn'
-      rw [hk, dissipate_succ, ← hk, hn, Set.inter_empty]
+      rw [hk, dissipate_def, dissipate_succ, ← hk, hn, Set.inter_empty]
 
 lemma directed_dissipate {s : ℕ → Set α} :
     Directed (fun (x1 x2 : Set α) => x2 ⊆ x1) (Dissipate s) :=
@@ -133,7 +132,7 @@ lemma exists_dissipate_eq_empty_iff_of_directed (C : ℕ → Set α)
     · rw [hn', dissipate_zero]
       exact hn' ▸ hn
     · obtain ⟨k, hk⟩ := exists_eq_succ_of_ne_zero hn'
-      simp_rw [hk, succ_eq_add_one, dissipate_succ,
+      simp_rw [hk, succ_eq_add_one, dissipate_def, dissipate_succ,
         ← succ_eq_add_one, ← hk, hn, Set.inter_empty]
   · rw [← not_imp_not]
     push_neg
@@ -151,7 +150,7 @@ lemma dissipate_of_piSystem {s : ℕ → Set α} {p : Set α → Prop}
     simp only [dissipate_def, le_zero_eq, iInter_iInter_eq_left]
     exact h 0
   | succ n hn =>
-    rw [dissipate_succ] at *
+    rw [dissipate_def, dissipate_succ] at *
     apply hp (Dissipate s n) (hn (Nonempty.left h')) (s (n+1)) (h (n+1)) h'
 
 end Set

From 662c21562a96d08a534dc8a862b3711acca4bba0 Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:04:47 +0200
Subject: [PATCH 29/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 7688d20a4e366c..48702470417d16 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -91,6 +91,7 @@ import Mathlib.Algebra.Category.BoolRing
 import Mathlib.Algebra.Category.CoalgCat.Basic
 import Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
 import Mathlib.Algebra.Category.CoalgCat.Monoidal
+import Mathlib.Algebra.Category.CommAlgCat.Basic
 import Mathlib.Algebra.Category.FGModuleCat.Basic
 import Mathlib.Algebra.Category.FGModuleCat.Limits
 import Mathlib.Algebra.Category.Grp.AB

From 6dd67ed29c27cf072ae4e2a5c4d7af1f8a180669 Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:04:59 +0200
Subject: [PATCH 30/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 48702470417d16..da429e215836d8 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5433,6 +5433,7 @@ import Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
 import Mathlib.RingTheory.Spectrum.Prime.Jacobson
 import Mathlib.RingTheory.Spectrum.Prime.Module
 import Mathlib.RingTheory.Spectrum.Prime.Noetherian
+import Mathlib.RingTheory.Spectrum.Prime.LTSeries
 import Mathlib.RingTheory.Spectrum.Prime.Polynomial
 import Mathlib.RingTheory.Spectrum.Prime.RingHom
 import Mathlib.RingTheory.Spectrum.Prime.TensorProduct

From f85265309c3f5e09b306cd8fb77f0e55a026792c Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:05:07 +0200
Subject: [PATCH 31/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index da429e215836d8..91d43fc91e00a0 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5613,6 +5613,7 @@ import Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
 import Mathlib.Tactic.CategoryTheory.Elementwise
 import Mathlib.Tactic.CategoryTheory.Monoidal.Basic
 import Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
+import Mathlib.Tactic.CategoryTheory.IsoReassoc
 import Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
 import Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
 import Mathlib.Tactic.CategoryTheory.MonoidalComp

From 6afe6111526d2f19ed6035b909d10710a39efcf7 Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:05:19 +0200
Subject: [PATCH 32/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 91d43fc91e00a0..e979c607dc670b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5913,6 +5913,7 @@ import Mathlib.Topology.Algebra.IsUniformGroup.Basic
 import Mathlib.Topology.Algebra.IsUniformGroup.Defs
 import Mathlib.Topology.Algebra.LinearTopology
 import Mathlib.Topology.Algebra.Localization
+import Mathlib.Topology.Algebra.IsUniformGroup.Order
 import Mathlib.Topology.Algebra.Module.Alternating.Basic
 import Mathlib.Topology.Algebra.Module.Alternating.Topology
 import Mathlib.Topology.Algebra.Module.Basic

From abba3bf44d08c543878d417c5c5aecfbc1fe9f04 Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:05:29 +0200
Subject: [PATCH 33/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index e979c607dc670b..77714afe1b116b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6072,6 +6072,8 @@ import Mathlib.Topology.CompactOpen
 import Mathlib.Topology.Compactification.OnePoint
 import Mathlib.Topology.Compactification.OnePointEquiv
 import Mathlib.Topology.Compactness.Bases
+import Mathlib.Topology.Compactification.OnePoint.Basic
+import Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
 import Mathlib.Topology.Compactness.Compact
 import Mathlib.Topology.Compactness.CompactSystem
 import Mathlib.Topology.Compactness.CompactlyGeneratedSpace

From eb54bcf111232bc4f2cbcb36caa3cc687f44b065 Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:05:40 +0200
Subject: [PATCH 34/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 77714afe1b116b..20afd0ea4e0980 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6078,6 +6078,7 @@ import Mathlib.Topology.Compactness.Compact
 import Mathlib.Topology.Compactness.CompactSystem
 import Mathlib.Topology.Compactness.CompactlyGeneratedSpace
 import Mathlib.Topology.Compactness.DeltaGeneratedSpace
+import Mathlib.Topology.Compactness.CompactlyCoherentSpace
 import Mathlib.Topology.Compactness.Exterior
 import Mathlib.Topology.Compactness.Lindelof
 import Mathlib.Topology.Compactness.LocallyCompact

From 3a83c6a5549e3f876eb427bc7982dbcb4f5ee6f8 Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:05:57 +0200
Subject: [PATCH 35/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 20afd0ea4e0980..d06d2f695e72fa 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1579,6 +1579,7 @@ import Mathlib.Analysis.InnerProductSpace.Spectrum
 import Mathlib.Analysis.InnerProductSpace.StarOrder
 import Mathlib.Analysis.InnerProductSpace.Subspace
 import Mathlib.Analysis.InnerProductSpace.Symmetric
+import Mathlib.Analysis.InnerProductSpace.Trace
 import Mathlib.Analysis.InnerProductSpace.TwoDim
 import Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
 import Mathlib.Analysis.InnerProductSpace.l2Space

From 8cd31bd0801b3328f9b0ad6040c93f5f6aff1756 Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:06:05 +0200
Subject: [PATCH 36/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index d06d2f695e72fa..4280f62b8fbb6e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1472,6 +1472,7 @@ import Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
 import Mathlib.Analysis.Complex.UpperHalfPlane.Metric
 import Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
 import Mathlib.Analysis.Complex.UpperHalfPlane.Topology
+import Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
 import Mathlib.Analysis.Complex.ValueDistribution.CountingFunction
 import Mathlib.Analysis.Complex.ValueDistribution.ProximityFunction
 import Mathlib.Analysis.ConstantSpeed

From 81b59ae10f3833f9a8bd0747c334b7692af01122 Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:06:13 +0200
Subject: [PATCH 37/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 4280f62b8fbb6e..27ad7571f0404d 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1312,6 +1312,7 @@ import Mathlib.Analysis.CStarAlgebra.CStarMatrix
 import Mathlib.Analysis.CStarAlgebra.Classes
 import Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

From 66109613dac9273e0d1c35f061068b82cc40fa3f Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:06:19 +0200
Subject: [PATCH 38/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 27ad7571f0404d..239e55c07735dd 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -93,6 +93,7 @@ import Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
 import Mathlib.Algebra.Category.CoalgCat.Monoidal
 import Mathlib.Algebra.Category.CommAlgCat.Basic
 import Mathlib.Algebra.Category.FGModuleCat.Basic
+import Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
 import Mathlib.Algebra.Category.FGModuleCat.Limits
 import Mathlib.Algebra.Category.Grp.AB
 import Mathlib.Algebra.Category.Grp.Abelian

From 7731bac41f86cdd0d0f8555a4abb4a441fef580b Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:08:31 +0200
Subject: [PATCH 39/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 239e55c07735dd..355f29f5a648d9 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1725,7 +1725,8 @@ import Mathlib.Analysis.NormedSpace.Multilinear.Basic
 import Mathlib.Analysis.NormedSpace.Multilinear.Curry
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic
-import Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear
+import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
+import Mathlib.Analysis.NormedSpace.Multilinear.Basic
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Mul
 import Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm

From 1f004f5d6cda28df99f47b11cba08f376ac03fef Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:09:05 +0200
Subject: [PATCH 40/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 355f29f5a648d9..480d3ddd449099 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2468,7 +2468,8 @@ import Mathlib.CategoryTheory.Shift.Induced
 import Mathlib.CategoryTheory.Shift.InducedShiftSequence
 import Mathlib.CategoryTheory.Shift.Localization
 import Mathlib.CategoryTheory.Shift.Opposite
-import Mathlib.CategoryTheory.Shift.Pullback
+import Mathlib.CategoryTheory.Shift.Linear
+import Mathlib.CategoryTheory.Shift.Induced
 import Mathlib.CategoryTheory.Shift.Quotient
 import Mathlib.CategoryTheory.Shift.ShiftSequence
 import Mathlib.CategoryTheory.Shift.ShiftedHom

From 2905ef6ff6419a4947f18119cf1bc8c228baa2f5 Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:09:16 +0200
Subject: [PATCH 41/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 480d3ddd449099..64681290848cda 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3137,7 +3137,8 @@ import Mathlib.Data.Matrix.Reflection
 import Mathlib.Data.Matrix.RowCol
 import Mathlib.Data.Matroid.Basic
 import Mathlib.Data.Matroid.Circuit
-import Mathlib.Data.Matroid.Closure
+import Mathlib.Data.Matrix.Vec
+import Mathlib.Data.Matrix.Reflection
 import Mathlib.Data.Matroid.Constructions
 import Mathlib.Data.Matroid.Dual
 import Mathlib.Data.Matroid.IndepAxioms

From b93d00cade8a18ea4cbed4f10794d7eb80b896f2 Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:09:24 +0200
Subject: [PATCH 42/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 64681290848cda..60d4a0eb60f3a8 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3855,7 +3855,8 @@ import Mathlib.LinearAlgebra.Alternating.Curry
 import Mathlib.LinearAlgebra.Alternating.DomCoprod
 import Mathlib.LinearAlgebra.AnnihilatingPolynomial
 import Mathlib.LinearAlgebra.Basis.Basic
-import Mathlib.LinearAlgebra.Basis.Bilinear
+import Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
+import Mathlib.LinearAlgebra.Alternating.Curry
 import Mathlib.LinearAlgebra.Basis.Cardinality
 import Mathlib.LinearAlgebra.Basis.Defs
 import Mathlib.LinearAlgebra.Basis.Exact

From eac2037b5dd7ba52a3244bfd823b9823ac5a8ddb Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:09:31 +0200
Subject: [PATCH 43/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 60d4a0eb60f3a8..d79ce98d141456 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4073,7 +4073,8 @@ import Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
 import Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
 import Mathlib.LinearAlgebra.RootSystem.Hom
 import Mathlib.LinearAlgebra.RootSystem.Irreducible
-import Mathlib.LinearAlgebra.RootSystem.IsValuedIn
+import Mathlib.LinearAlgebra.RootSystem.GeckConstruction
+import Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
 import Mathlib.LinearAlgebra.RootSystem.OfBilinear
 import Mathlib.LinearAlgebra.RootSystem.Reduced
 import Mathlib.LinearAlgebra.RootSystem.RootPairingCat

From 4a94a1285b54e082740ab19a06a1ad07df2de7e5 Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:09:59 +0200
Subject: [PATCH 44/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index d79ce98d141456..18148bad893e82 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5444,7 +5444,6 @@ import Mathlib.RingTheory.Spectrum.Prime.Module
 import Mathlib.RingTheory.Spectrum.Prime.Noetherian
 import Mathlib.RingTheory.Spectrum.Prime.LTSeries
 import Mathlib.RingTheory.Spectrum.Prime.Polynomial
-import Mathlib.RingTheory.Spectrum.Prime.RingHom
 import Mathlib.RingTheory.Spectrum.Prime.TensorProduct
 import Mathlib.RingTheory.Spectrum.Prime.Topology
 import Mathlib.RingTheory.Support

From 57f06e0e7382fb481792eca7692926be7aba097f Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:10:09 +0200
Subject: [PATCH 45/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 18148bad893e82..b2a93e50cafcad 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5622,6 +5622,7 @@ import Mathlib.Tactic.CategoryTheory.Elementwise
 import Mathlib.Tactic.CategoryTheory.Monoidal.Basic
 import Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
 import Mathlib.Tactic.CategoryTheory.IsoReassoc
+import Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
 import Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
 import Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
 import Mathlib.Tactic.CategoryTheory.MonoidalComp

From de14766c8d6e738009ec66293c1d2e9804183b0a Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:10:51 +0200
Subject: [PATCH 46/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index b2a93e50cafcad..010da8d5afb722 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6089,7 +6089,6 @@ import Mathlib.Topology.Compactness.CompactlyGeneratedSpace
 import Mathlib.Topology.Compactness.DeltaGeneratedSpace
 import Mathlib.Topology.Compactness.CompactlyCoherentSpace
 import Mathlib.Topology.Compactness.Exterior
-import Mathlib.Topology.Compactness.Lindelof
 import Mathlib.Topology.Compactness.LocallyCompact
 import Mathlib.Topology.Compactness.LocallyFinite
 import Mathlib.Topology.Compactness.Paracompact

From 3edbee24119ede59a6b5c107ff068d8b94ac15fd Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:11:04 +0200
Subject: [PATCH 47/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 010da8d5afb722..065e7bf7eef377 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6088,6 +6088,7 @@ import Mathlib.Topology.Compactness.CompactSystem
 import Mathlib.Topology.Compactness.CompactlyGeneratedSpace
 import Mathlib.Topology.Compactness.DeltaGeneratedSpace
 import Mathlib.Topology.Compactness.CompactlyCoherentSpace
+import Mathlib.Topology.Compactness.Compact
 import Mathlib.Topology.Compactness.Exterior
 import Mathlib.Topology.Compactness.LocallyCompact
 import Mathlib.Topology.Compactness.LocallyFinite

From 56be952e48ec2e031b5b91484bd19d780ac1042a Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:11:56 +0200
Subject: [PATCH 48/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 065e7bf7eef377..6b72b317d56df1 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3857,8 +3857,7 @@ import Mathlib.LinearAlgebra.AnnihilatingPolynomial
 import Mathlib.LinearAlgebra.Basis.Basic
 import Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
 import Mathlib.LinearAlgebra.Alternating.Curry
-import Mathlib.LinearAlgebra.Basis.Cardinality
-import Mathlib.LinearAlgebra.Basis.Defs
+import Mathlib.LinearAlgebra.Basis.Bilinear
 import Mathlib.LinearAlgebra.Basis.Exact
 import Mathlib.LinearAlgebra.Basis.Fin
 import Mathlib.LinearAlgebra.Basis.Flag

From 1949b3bb6bcdc1a50c03f95d9ff06cfc534ee8b8 Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Thu, 5 Jun 2025 00:12:09 +0200
Subject: [PATCH 49/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 6b72b317d56df1..bd64a0b04e8b87 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6087,6 +6087,7 @@ import Mathlib.Topology.Compactness.CompactSystem
 import Mathlib.Topology.Compactness.CompactlyGeneratedSpace
 import Mathlib.Topology.Compactness.DeltaGeneratedSpace
 import Mathlib.Topology.Compactness.CompactlyCoherentSpace
+import Mathlib.Topology.Compactness.DeltaGeneratedSpace
 import Mathlib.Topology.Compactness.Compact
 import Mathlib.Topology.Compactness.Exterior
 import Mathlib.Topology.Compactness.LocallyCompact

From 783c0c3e7a34a48b3a860d6857be6789c31ff5e9 Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Sat, 7 Jun 2025 23:36:46 +0200
Subject: [PATCH 50/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index bd64a0b04e8b87..21491caeb248d4 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1726,6 +1726,7 @@ import Mathlib.Analysis.NormedSpace.Multilinear.Curry
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic
 import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
+import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
 import Mathlib.Analysis.NormedSpace.Multilinear.Basic
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Mul

From 32439d48700f8b028086cf1011f7cdeca6d1cc55 Mon Sep 17 00:00:00 2001
From: Peter Pfaffelhuber <41927422+pfaffelh@users.noreply.github.com>
Date: Sat, 7 Jun 2025 23:37:09 +0200
Subject: [PATCH 51/53] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 21491caeb248d4..2ace64fcb5c549 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1728,8 +1728,7 @@ import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic
 import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
 import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
 import Mathlib.Analysis.NormedSpace.Multilinear.Basic
-import Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness
-import Mathlib.Analysis.NormedSpace.OperatorNorm.Mul
+import Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear
 import Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm
 import Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Prod

From 96ef30d6fdf3c452e1eec2b35b0bfe76c9eb009b Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Sat, 7 Jun 2025 23:39:39 +0200
Subject: [PATCH 52/53] fix two typos

---
 Mathlib/Topology/Compactness/CompactSystem.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Topology/Compactness/CompactSystem.lean b/Mathlib/Topology/Compactness/CompactSystem.lean
index 17c4fc989626ce..dd520e7a1026e4 100644
--- a/Mathlib/Topology/Compactness/CompactSystem.lean
+++ b/Mathlib/Topology/Compactness/CompactSystem.lean
@@ -9,7 +9,7 @@ import Mathlib.Topology.Separation.Hausdorff
 /-!
 # Compact systems.
 
-This files defines compact systems of sets.
+This file defines compact systems of sets.
 
 ## Main definitions
 
@@ -162,7 +162,7 @@ lemma iff_isCompactSystem_of_or_univ : IsCompactSystem p ↔
             simp only [h₆, Set.mem_univ]
       have h₇ : Dissipate s' (max j n) = ∅ := by
         rw [← subset_empty_iff] at hj ⊢
-        exact le_trans (antitone_dissipate (Nat.le_max_left j n)) hj
+        exact le_trans (dissipate_antitone (Nat.le_max_left j n)) hj
       specialize h₂ (max j n) (Nat.le_max_right j n)
       specialize hd (max j n)
       rw [h₂, Set.nonempty_iff_ne_empty, h₇] at hd
@@ -242,7 +242,7 @@ theorem of_isCompact_isClosed :
   have htco : ∀ (i : { j : ℕ | s j ≠ univ}), IsCompact (s i) :=
     fun i ↦ (h1 i).1
   haveI f : Nonempty α := by
-    apply nonempty_of_exists _
+    apply Exists.nonempty _
     · exact fun x ↦ x ∈ s 0
     · exact h2 0
   by_cases h : Nonempty ↑{j | s j ≠ Set.univ}

From f16b9dc48ee8fdee95789b45ea831f901f06cb2d Mon Sep 17 00:00:00 2001
From: pfaffelh <pfaffelh@gmail.com>
Date: Sun, 8 Jun 2025 19:51:50 +0200
Subject: [PATCH 53/53] mk_all

---
 Mathlib.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index c985dd059537e6..2448d9a560ce20 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3374,6 +3374,7 @@ import Mathlib.Data.Set.Constructions
 import Mathlib.Data.Set.Countable
 import Mathlib.Data.Set.Defs
 import Mathlib.Data.Set.Disjoint
+import Mathlib.Data.Set.Dissipate
 import Mathlib.Data.Set.Enumerate
 import Mathlib.Data.Set.Equitable
 import Mathlib.Data.Set.Finite.Basic
@@ -6104,6 +6105,7 @@ import Mathlib.Topology.Compactification.OnePoint.Sphere
 import Mathlib.Topology.Compactification.OnePointEquiv
 import Mathlib.Topology.Compactness.Bases
 import Mathlib.Topology.Compactness.Compact
+import Mathlib.Topology.Compactness.CompactSystem
 import Mathlib.Topology.Compactness.CompactlyCoherentSpace
 import Mathlib.Topology.Compactness.CompactlyGeneratedSpace
 import Mathlib.Topology.Compactness.DeltaGeneratedSpace