From 6cccdd464364694502ff461e53ed9a6080728b39 Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Sat, 2 Aug 2025 21:57:15 +0800
Subject: [PATCH 1/7] Initial commit (orphan branch)


From 7803007c25675bd530bdb4028b7d29e39e07b808 Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Thu, 25 Dec 2025 23:27:58 -0500
Subject: [PATCH 2/7] Update Lemmas.lean

---
 Mathlib/Topology/Baire/Lemmas.lean | 31 +++++++++++++++++++++++++++++-
 1 file changed, 30 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Baire/Lemmas.lean b/Mathlib/Topology/Baire/Lemmas.lean
index 652817cc324a84..e93e2d83d4abd3 100644
--- a/Mathlib/Topology/Baire/Lemmas.lean
+++ b/Mathlib/Topology/Baire/Lemmas.lean
@@ -6,6 +6,8 @@ Authors: Sébastien Gouëzel
 module
 
 public import Mathlib.Topology.GDelta.Basic
+public import Mathlib.Topology.Defs.Induced
+public import Mathlib.Topology.LocallyFinite
 
 /-!
 # Baire spaces
@@ -40,7 +42,34 @@ variable {X α : Type*} {ι : Sort*}
 
 section BaireTheorem
 
-variable [TopologicalSpace X] [BaireSpace X]
+variable [TopologicalSpace X]
+
+theorem baire_of_finite [Finite X] : BaireSpace X := by sorry
+
+/-- If a space `X` contains a dense Baire subspace, then `X` is Baire. -/
+theorem Dense.baire_mono {s : Set X} (hd : Dense s) (hb : BaireSpace s) : BaireSpace X := by
+  sorry
+
+/-- The union of an arbitrary family of open Baire subspaces is Baire. -/
+theorem baire_of_union_open_baire {s : α → Set X} (hs : ∀ a, IsOpen (s a))
+    (hb : ∀ a, BaireSpace (s a)) : BaireSpace (⋃ a, s a) := by
+  sorry
+
+/-- The union of a finite union of Baire subspaces is Baire. -/
+theorem baire_of_finite_union_baire {s : α → Set X} [Finite α] (hb : ∀ a, BaireSpace (s a)) :
+    BaireSpace (⋃ a, s a) := by
+  sorry
+
+/-- The union of a locally finite collection of Baire subspaces is Baire. -/
+theorem LocallyFinite.baire_of_union_baire {s : α → Set X} (hs : LocallyFinite s)
+    (hb : ∀ a, BaireSpace (s a)) : BaireSpace (⋃ a, s a) := by
+  sorry
+
+/-- If each point of `X` has a Baire neighborhood, then `X` is Baire. -/
+theorem baire_of_nhds_baire (hx : ∀ x : X, ∃ U ∈ 𝓝 x, BaireSpace U) : BaireSpace X := by
+  sorry
+
+variable [BaireSpace X]
 
 /-- Definition of a Baire space. -/
 theorem dense_iInter_of_isOpen_nat {f : ℕ → Set X} (ho : ∀ n, IsOpen (f n))

From 16f72a4ffe7979270d2f47658590dce060e88b75 Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Fri, 26 Dec 2025 01:30:01 -0500
Subject: [PATCH 3/7] Update Lemmas.lean

---
 Mathlib/Topology/Baire/Lemmas.lean | 46 ++++++++++++++----------------
 1 file changed, 21 insertions(+), 25 deletions(-)

diff --git a/Mathlib/Topology/Baire/Lemmas.lean b/Mathlib/Topology/Baire/Lemmas.lean
index e93e2d83d4abd3..9d72a938962570 100644
--- a/Mathlib/Topology/Baire/Lemmas.lean
+++ b/Mathlib/Topology/Baire/Lemmas.lean
@@ -6,7 +6,6 @@ Authors: Sébastien Gouëzel
 module
 
 public import Mathlib.Topology.GDelta.Basic
-public import Mathlib.Topology.Defs.Induced
 public import Mathlib.Topology.LocallyFinite
 
 /-!
@@ -44,30 +43,25 @@ section BaireTheorem
 
 variable [TopologicalSpace X]
 
-theorem baire_of_finite [Finite X] : BaireSpace X := by sorry
-
-/-- If a space `X` contains a dense Baire subspace, then `X` is Baire. -/
-theorem Dense.baire_mono {s : Set X} (hd : Dense s) (hb : BaireSpace s) : BaireSpace X := by
-  sorry
-
-/-- The union of an arbitrary family of open Baire subspaces is Baire. -/
-theorem baire_of_union_open_baire {s : α → Set X} (hs : ∀ a, IsOpen (s a))
-    (hb : ∀ a, BaireSpace (s a)) : BaireSpace (⋃ a, s a) := by
-  sorry
-
-/-- The union of a finite union of Baire subspaces is Baire. -/
-theorem baire_of_finite_union_baire {s : α → Set X} [Finite α] (hb : ∀ a, BaireSpace (s a)) :
-    BaireSpace (⋃ a, s a) := by
-  sorry
-
-/-- The union of a locally finite collection of Baire subspaces is Baire. -/
-theorem LocallyFinite.baire_of_union_baire {s : α → Set X} (hs : LocallyFinite s)
-    (hb : ∀ a, BaireSpace (s a)) : BaireSpace (⋃ a, s a) := by
-  sorry
-
-/-- If each point of `X` has a Baire neighborhood, then `X` is Baire. -/
-theorem baire_of_nhds_baire (hx : ∀ x : X, ∃ U ∈ 𝓝 x, BaireSpace U) : BaireSpace X := by
-  sorry
+/-- The intersection of finitely many open dense sets is dense. -/
+theorem Set.Finite.Dense_sInter {s : Set (Set X)} (hs : s.Finite)
+    (ho : ∀ t ∈ s, IsOpen t) (hd : ∀ t ∈ s, Dense t) : Dense (⋂₀ s) := by
+  induction s, hs using Set.Finite.induction_on with
+  | empty => simp [sInter_empty]
+  | insert ha hsf ih =>
+    simp only [sInter_insert, forall_mem_insert] at hd ⊢
+    refine hd.1.inter_of_isOpen_right ?_ (hsf.isOpen_sInter (fun y hy => ho y (Or.inr hy)))
+    exact ih ((fun y hy => ho y (Or.inr hy))) (fun y hy => hd.2 y hy)
+
+/-- A finite set is Baire. -/
+theorem baire_of_finite [Finite X] : BaireSpace X := by
+  constructor
+  refine fun f hof hdf => (sInter_range f) ▸ Set.Finite.Dense_sInter
+    (Finite.subset Set.finite_univ (subset_univ (range f))) (fun _ h => ?_) (fun _ h => ?_)
+  · obtain ⟨x, hx⟩ := h
+    simpa [← hx] using hof x
+  · obtain ⟨x, hx⟩ := h
+    simpa [← hx] using hdf x
 
 variable [BaireSpace X]
 
@@ -228,3 +222,5 @@ theorem not_isMeagre_of_mem_residual {s : Set X} (hs : s ∈ residual X) :
   exact not_isMeagre_of_isGδ_of_dense (X := X) htGδ ht_dense (hs_meagre.mono ht_sub)
 
 end BaireTheorem
+
+#min_imports

From d7020aeae78c909262261eb0a3baba54ca99cf94 Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Fri, 26 Dec 2025 01:32:06 -0500
Subject: [PATCH 4/7] Update Lemmas.lean

---
 Mathlib/Topology/Baire/Lemmas.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Topology/Baire/Lemmas.lean b/Mathlib/Topology/Baire/Lemmas.lean
index 9d72a938962570..c045901e4d3693 100644
--- a/Mathlib/Topology/Baire/Lemmas.lean
+++ b/Mathlib/Topology/Baire/Lemmas.lean
@@ -5,8 +5,9 @@ Authors: Sébastien Gouëzel
 -/
 module
 
+public import Mathlib.Data.Fintype.Powerset
 public import Mathlib.Topology.GDelta.Basic
-public import Mathlib.Topology.LocallyFinite
+public import Mathlib.Topology.Neighborhoods
 
 /-!
 # Baire spaces
@@ -222,5 +223,3 @@ theorem not_isMeagre_of_mem_residual {s : Set X} (hs : s ∈ residual X) :
   exact not_isMeagre_of_isGδ_of_dense (X := X) htGδ ht_dense (hs_meagre.mono ht_sub)
 
 end BaireTheorem
-
-#min_imports

From 0346d7f350cd8422778e42461713cc96aaea3f57 Mon Sep 17 00:00:00 2001
From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com>
Date: Wed, 31 Dec 2025 15:22:44 -0500
Subject: [PATCH 5/7] Update Mathlib/Topology/Baire/Lemmas.lean

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
---
 Mathlib/Topology/Baire/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Baire/Lemmas.lean b/Mathlib/Topology/Baire/Lemmas.lean
index 5f0f7d244c297c..8ed2bde1f4aed2 100644
--- a/Mathlib/Topology/Baire/Lemmas.lean
+++ b/Mathlib/Topology/Baire/Lemmas.lean
@@ -45,7 +45,7 @@ section BaireTheorem
 variable [TopologicalSpace X]
 
 /-- The intersection of finitely many open dense sets is dense. -/
-theorem Set.Finite.Dense_sInter {s : Set (Set X)} (hs : s.Finite)
+theorem Set.Finite.dense_sInter {s : Set (Set X)} (hs : s.Finite)
     (ho : ∀ t ∈ s, IsOpen t) (hd : ∀ t ∈ s, Dense t) : Dense (⋂₀ s) := by
   induction s, hs using Set.Finite.induction_on with
   | empty => simp [sInter_empty]

From 183abd14a136f4f00ebe9843bcefbb4a9708aca6 Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Wed, 31 Dec 2025 15:26:22 -0500
Subject: [PATCH 6/7] Update Lemmas.lean

---
 Mathlib/Topology/Baire/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Baire/Lemmas.lean b/Mathlib/Topology/Baire/Lemmas.lean
index 8ed2bde1f4aed2..cf685132458b06 100644
--- a/Mathlib/Topology/Baire/Lemmas.lean
+++ b/Mathlib/Topology/Baire/Lemmas.lean
@@ -57,7 +57,7 @@ theorem Set.Finite.dense_sInter {s : Set (Set X)} (hs : s.Finite)
 /-- A finite set is Baire. -/
 theorem baire_of_finite [Finite X] : BaireSpace X := by
   constructor
-  refine fun f hof hdf => (sInter_range f) ▸ Set.Finite.Dense_sInter
+  refine fun f hof hdf => (sInter_range f) ▸ Set.Finite.dense_sInter
     (Finite.subset Set.finite_univ (subset_univ (range f))) (fun _ h => ?_) (fun _ h => ?_)
   · obtain ⟨x, hx⟩ := h
     simpa [← hx] using hof x

From 53df2ae15cb48321a46e2ea2848db92e94f3f996 Mon Sep 17 00:00:00 2001
From: Rmal <97214596+CoolRmal@users.noreply.github.com>
Date: Wed, 31 Dec 2025 15:27:35 -0500
Subject: [PATCH 7/7] Update Lemmas.lean

---
 Mathlib/Topology/Baire/Lemmas.lean | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Topology/Baire/Lemmas.lean b/Mathlib/Topology/Baire/Lemmas.lean
index cf685132458b06..5095bca5a1e8f1 100644
--- a/Mathlib/Topology/Baire/Lemmas.lean
+++ b/Mathlib/Topology/Baire/Lemmas.lean
@@ -55,14 +55,8 @@ theorem Set.Finite.dense_sInter {s : Set (Set X)} (hs : s.Finite)
     exact ih ((fun y hy => ho y (Or.inr hy))) (fun y hy => hd.2 y hy)
 
 /-- A finite set is Baire. -/
-theorem baire_of_finite [Finite X] : BaireSpace X := by
-  constructor
-  refine fun f hof hdf => (sInter_range f) ▸ Set.Finite.dense_sInter
-    (Finite.subset Set.finite_univ (subset_univ (range f))) (fun _ h => ?_) (fun _ h => ?_)
-  · obtain ⟨x, hx⟩ := h
-    simpa [← hx] using hof x
-  · obtain ⟨x, hx⟩ := h
-    simpa [← hx] using hdf x
+theorem baire_of_finite [Finite X] : BaireSpace X where
+  baire_property f _ _ := sInter_range f ▸ (toFinite (range f)).dense_sInter (by grind) (by grind)
 
 variable [BaireSpace X]