chore: split MetricSpace/Baire (#10648)

* move definition to `Topology/Defs/Basic`;
* move lemmas to `Topology/Baire/Lemmas`;
* move instances to `Topology/Baire/CompleteMetrizable` and `Topology/Baire/LocallyCompactRegular`;
* assume `[UniformSpace X] [IsCountablyGenerated (𝓤 X)]` instead of `[PseudoMetricSpace X]` in the 1st theorem.

This way `Lemmas` file does not depend on analysis.

Counterexamples/SorgenfreyLine.lean

@@ -10,7 +10,8 @@ import Mathlib.Topology.Metrizable.Urysohn
 import Mathlib.Topology.EMetricSpace.Paracompact
 import Mathlib.Data.Set.Intervals.Monotone
 import Mathlib.Topology.Separation.NotNormal
-import Mathlib.Topology.MetricSpace.Baire
+import Mathlib.Topology.Baire.Lemmas
+import Mathlib.Topology.Baire.LocallyCompactRegular
 
 #align_import sorgenfrey_line from "leanprover-community/mathlib"@"328375597f2c0dd00522d9c2e5a33b6a6128feeb"
 

Mathlib.lean

@@ -3738,6 +3738,9 @@ import Mathlib.Topology.Algebra.UniformRing
 import Mathlib.Topology.Algebra.Valuation
 import Mathlib.Topology.Algebra.ValuedField
 import Mathlib.Topology.Algebra.WithZeroTopology
+import Mathlib.Topology.Baire.CompleteMetrizable
+import Mathlib.Topology.Baire.Lemmas
+import Mathlib.Topology.Baire.LocallyCompactRegular
 import Mathlib.Topology.Bases
 import Mathlib.Topology.Basic
 import Mathlib.Topology.Bornology.Absorbs
@@ -3870,7 +3873,6 @@ import Mathlib.Topology.LocallyFinite
 import Mathlib.Topology.Maps
 import Mathlib.Topology.MetricSpace.Algebra
 import Mathlib.Topology.MetricSpace.Antilipschitz
-import Mathlib.Topology.MetricSpace.Baire
 import Mathlib.Topology.MetricSpace.Basic
 import Mathlib.Topology.MetricSpace.Bounded
 import Mathlib.Topology.MetricSpace.CantorScheme

Mathlib/Analysis/LocallyConvex/Barrelled.lean

@@ -5,7 +5,7 @@ Authors: Anatole Dedecker
 -/
 import Mathlib.Analysis.LocallyConvex.WithSeminorms
 import Mathlib.Topology.Semicontinuous
-import Mathlib.Topology.MetricSpace.Baire
+import Mathlib.Topology.Baire.Lemmas
 
 /-!
 # Barrelled spaces and the Banach-Steinhaus theorem / Uniform Boundedness Principle

Mathlib/Analysis/NormedSpace/Banach.lean

@@ -3,7 +3,8 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.Topology.MetricSpace.Baire
+import Mathlib.Topology.Baire.Lemmas
+import Mathlib.Topology.Baire.CompleteMetrizable
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic
 import Mathlib.Analysis.NormedSpace.AffineIsometry
 import Mathlib.Analysis.Normed.Group.InfiniteSum

Mathlib/Analysis/NormedSpace/BanachSteinhaus.lean

@@ -5,6 +5,7 @@ Authors: Jireh Loreaux
 -/
 import Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace
 import Mathlib.Analysis.LocallyConvex.Barrelled
+import Mathlib.Topology.Baire.CompleteMetrizable
 
 #align_import analysis.normed_space.banach_steinhaus from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
 

Mathlib/NumberTheory/Liouville/Residual.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.NumberTheory.Liouville.Basic
-import Mathlib.Topology.MetricSpace.Baire
+import Mathlib.Topology.Baire.Lemmas
+import Mathlib.Topology.Baire.LocallyCompactRegular
 import Mathlib.Topology.Instances.Irrational
 
 #align_import number_theory.liouville.residual from "leanprover-community/mathlib"@"32b08ef840dd25ca2e47e035c5da03ce16d2dc3c"

Mathlib/Topology/Algebra/Group/OpenMapping.lean

@@ -3,7 +3,8 @@ Copyright (c) 2023 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.Topology.MetricSpace.Baire
+import Mathlib.Topology.Baire.Lemmas
+import Mathlib.Topology.Algebra.Group.Basic
 
 /-! # Open mapping theorem for morphisms of topological groups
 

Mathlib/Topology/Baire/CompleteMetrizable.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel, Yury Kudryashov
+-/
+import Mathlib.Analysis.SpecificLimits.Basic
+import Mathlib.Topology.Metrizable.Uniformity
+
+#align_import topology.metric_space.baire from "leanprover-community/mathlib"@"b9e46fe101fc897fb2e7edaf0bf1f09ea49eb81a"
+
+/-!
+# First Baire theorem
+
+In this file we prove that a completely metrizable topological space is a Baire space.
+Since `Mathlib` does not have the notion of a completely metrizable topological space yet,
+we state it for a complete uniform space with countably generated uniformity filter.
+-/
+
+open Filter EMetric Set
+open scoped Topology Uniformity ENNReal
+
+variable {X : Type*} [UniformSpace X] [CompleteSpace X] [(𝓤 X).IsCountablyGenerated]
+
+/-- **First Baire theorem**: a completely metrizable topological space has Baire property.
+
+Since `Mathlib` does not have the notion of a completely metrizable topological space yet,
+we state it for a complete uniform space with countably generated uniformity filter. -/
+instance (priority := 100) BaireSpace.of_pseudoEMetricSpace_completeSpace : BaireSpace X := by
+  let _ := UniformSpace.pseudoMetricSpace X
+  refine' ⟨fun f ho hd => _⟩
+  let B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
+  have Bpos : ∀ n, 0 < B n := fun n ↦
+    ENNReal.div_pos one_ne_zero <| ENNReal.pow_ne_top ENNReal.coe_ne_top
+  /- Translate the density assumption into two functions `center` and `radius` associating
+    to any n, x, δ, δpos a center and a positive radius such that
+    `closedBall center radius` is included both in `f n` and in `closedBall x δ`.
+    We can also require `radius ≤ (1/2)^(n+1)`, to ensure we get a Cauchy sequence later. -/
+  have : ∀ n x δ, δ ≠ 0 → ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedBall y r ⊆ closedBall x δ ∩ f n := by
+    intro n x δ δpos
+    have : x ∈ closure (f n) := hd n x
+    rcases EMetric.mem_closure_iff.1 this (δ / 2) (ENNReal.half_pos δpos) with ⟨y, ys, xy⟩
+    rw [edist_comm] at xy
+    obtain ⟨r, rpos, hr⟩ : ∃ r > 0, closedBall y r ⊆ f n :=
+      nhds_basis_closed_eball.mem_iff.1 (isOpen_iff_mem_nhds.1 (ho n) y ys)
+    refine' ⟨y, min (min (δ / 2) r) (B (n + 1)), _, _, fun z hz => ⟨_, _⟩⟩
+    show 0 < min (min (δ / 2) r) (B (n + 1))
+    exact lt_min (lt_min (ENNReal.half_pos δpos) rpos) (Bpos (n + 1))
+    show min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
+    exact min_le_right _ _
+    show z ∈ closedBall x δ
+    exact
+      calc
+        edist z x ≤ edist z y + edist y x := edist_triangle _ _ _
+        _ ≤ min (min (δ / 2) r) (B (n + 1)) + δ / 2 := (add_le_add hz (le_of_lt xy))
+        _ ≤ δ / 2 + δ / 2 := (add_le_add (le_trans (min_le_left _ _) (min_le_left _ _)) le_rfl)
+        _ = δ := ENNReal.add_halves δ
+    show z ∈ f n
+    exact hr (calc
+      edist z y ≤ min (min (δ / 2) r) (B (n + 1)) := hz
+      _ ≤ r := le_trans (min_le_left _ _) (min_le_right _ _))
+  choose! center radius Hpos HB Hball using this
+  refine' fun x => (mem_closure_iff_nhds_basis nhds_basis_closed_eball).2 fun ε εpos => _
+  /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x` belonging to all
+    `f n`. For this, we construct inductively a sequence `F n = (c n, r n)` such that the closed
+    ball `closedBall (c n) (r n)` is included in the previous ball and in `f n`, and such that
+    `r n` is small enough to ensure that `c n` is a Cauchy sequence. Then `c n` converges to a
+    limit which belongs to all the `f n`. -/
+  let F : ℕ → X × ℝ≥0∞ := fun n =>
+    Nat.recOn n (Prod.mk x (min ε (B 0))) fun n p => Prod.mk (center n p.1 p.2) (radius n p.1 p.2)
+  let c : ℕ → X := fun n => (F n).1
+  let r : ℕ → ℝ≥0∞ := fun n => (F n).2
+  have rpos : ∀ n, 0 < r n := by
+    intro n
+    induction' n with n hn
+    exact lt_min εpos (Bpos 0)
+    exact Hpos n (c n) (r n) hn.ne'
+  have r0 : ∀ n, r n ≠ 0 := fun n => (rpos n).ne'
+  have rB : ∀ n, r n ≤ B n := by
+    intro n
+    induction' n with n _
+    exact min_le_right _ _
+    exact HB n (c n) (r n) (r0 n)
+  have incl : ∀ n, closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n :=
+    fun n => Hball n (c n) (r n) (r0 n)
+  have cdist : ∀ n, edist (c n) (c (n + 1)) ≤ B n := by
+    intro n
+    rw [edist_comm]
+    have A : c (n + 1) ∈ closedBall (c (n + 1)) (r (n + 1)) := mem_closedBall_self
+    have I :=
+      calc
+        closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) :=
+          Subset.trans (incl n) (inter_subset_left _ _)
+        _ ⊆ closedBall (c n) (B n) := closedBall_subset_closedBall (rB n)
+    exact I A
+  have : CauchySeq c := cauchySeq_of_edist_le_geometric_two _ ENNReal.one_ne_top cdist
+  -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`.
+  rcases cauchySeq_tendsto_of_complete this with ⟨y, ylim⟩
+  -- this point `y` will be the desired point. We will check that it belongs to all
+  -- `f n` and to `ball x ε`.
+  use y
+  simp only [exists_prop, Set.mem_iInter]
+  have I : ∀ n, ∀ m ≥ n, closedBall (c m) (r m) ⊆ closedBall (c n) (r n) := by
+    intro n
+    refine' Nat.le_induction _ fun m _ h => _
+    · exact Subset.refl _
+    · exact Subset.trans (incl m) (Subset.trans (inter_subset_left _ _) h)
+  have yball : ∀ n, y ∈ closedBall (c n) (r n) := by
+    intro n
+    refine' isClosed_ball.mem_of_tendsto ylim _
+    refine' (Filter.eventually_ge_atTop n).mono fun m hm => _
+    exact I n m hm mem_closedBall_self
+  constructor
+  show ∀ n, y ∈ f n
+  · intro n
+    have : closedBall (c (n + 1)) (r (n + 1)) ⊆ f n :=
+      Subset.trans (incl n) (inter_subset_right _ _)
+    exact this (yball (n + 1))
+  show edist y x ≤ ε
+  exact le_trans (yball 0) (min_le_left _ _)
+#align baire_category_theorem_emetric_complete BaireSpace.of_pseudoEMetricSpace_completeSpace
+

Mathlib/Topology/MetricSpace/Baire.lean → Mathlib/Topology/Baire/Lemmas.lean

@@ -3,22 +3,26 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.Analysis.SpecificLimits.Basic
-import Mathlib.Order.Filter.CountableInter
 import Mathlib.Topology.GDelta
-import Mathlib.Topology.Sets.Compacts
 
 #align_import topology.metric_space.baire from "leanprover-community/mathlib"@"b9e46fe101fc897fb2e7edaf0bf1f09ea49eb81a"
 
 /-!
-# Baire theorem
+# Baire spaces
 
-In a complete metric space, a countable intersection of dense open subsets is dense.
+A topological space is called a *Baire space*
+if a countable intersection of dense open subsets is dense.
+Baire theorems say that all completely metrizable spaces
+and all locally compact regular spaces are Baire spaces.
+We prove the theorems in `Mathlib/Topology/Baire/CompleteMetrizable`
+and `Mathlib/Topology/Baire/LocallyCompactRegular`.
 
-The good concept underlying the theorem is that of a Gδ set, i.e., a countable intersection
+In this file we prove various corollaries of Baire theorems.
+
+The good concept underlying the theorems is that of a Gδ set, i.e., a countable intersection
 of open sets. Then Baire theorem can also be formulated as the fact that a countable
-intersection of dense Gδ sets is a dense Gδ set. We prove Baire theorem, giving several different
-formulations that can be handy. We also prove the important consequence that, if the space is
+intersection of dense Gδ sets is a dense Gδ set. We deduce this version from Baire property.
+We also prove the important consequence that, if the space is
 covered by a countable union of closed sets, then the union of their interiors is dense.
 
 We also prove that in Baire spaces, the `residual` sets are exactly those containing a dense Gδ set.
@@ -27,160 +31,13 @@ We also prove that in Baire spaces, the `residual` sets are exactly those contai
 
 noncomputable section
 
-open scoped Classical Topology Filter ENNReal
-
+open scoped Topology
 open Filter Set TopologicalSpace
 
 variable {X α : Type*} {ι : Sort*}
 
 section BaireTheorem
 
-open EMetric ENNReal
-
-/-- The property `BaireSpace α` means that the topological space `α` has the Baire property:
-any countable intersection of open dense subsets is dense.
-Formulated here when the source space is ℕ (and subsumed below by `dense_iInter_of_isOpen` working
-with any encodable source space). -/
-class BaireSpace (X : Type*) [TopologicalSpace X] : Prop where
-  baire_property : ∀ f : ℕ → Set X, (∀ n, IsOpen (f n)) → (∀ n, Dense (f n)) → Dense (⋂ n, f n)
-#align baire_space BaireSpace
-
-/-- Baire theorems asserts that various topological spaces have the Baire property.
-Two versions of these theorems are given.
-The first states that complete `PseudoEMetricSpace`s are Baire. -/
-instance (priority := 100) BaireSpace.of_pseudoEMetricSpace_completeSpace [PseudoEMetricSpace X]
-    [CompleteSpace X] : BaireSpace X := by
-  refine' ⟨fun f ho hd => _⟩
-  let B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
-  have Bpos : ∀ n, 0 < B n := fun n ↦
-    ENNReal.div_pos one_ne_zero <| ENNReal.pow_ne_top ENNReal.coe_ne_top
-  /- Translate the density assumption into two functions `center` and `radius` associating
-    to any n, x, δ, δpos a center and a positive radius such that
-    `closedBall center radius` is included both in `f n` and in `closedBall x δ`.
-    We can also require `radius ≤ (1/2)^(n+1)`, to ensure we get a Cauchy sequence later. -/
-  have : ∀ n x δ, δ ≠ 0 → ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedBall y r ⊆ closedBall x δ ∩ f n := by
-    intro n x δ δpos
-    have : x ∈ closure (f n) := hd n x
-    rcases EMetric.mem_closure_iff.1 this (δ / 2) (ENNReal.half_pos δpos) with ⟨y, ys, xy⟩
-    rw [edist_comm] at xy
-    obtain ⟨r, rpos, hr⟩ : ∃ r > 0, closedBall y r ⊆ f n :=
-      nhds_basis_closed_eball.mem_iff.1 (isOpen_iff_mem_nhds.1 (ho n) y ys)
-    refine' ⟨y, min (min (δ / 2) r) (B (n + 1)), _, _, fun z hz => ⟨_, _⟩⟩
-    show 0 < min (min (δ / 2) r) (B (n + 1))
-    exact lt_min (lt_min (ENNReal.half_pos δpos) rpos) (Bpos (n + 1))
-    show min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
-    exact min_le_right _ _
-    show z ∈ closedBall x δ
-    exact
-      calc
-        edist z x ≤ edist z y + edist y x := edist_triangle _ _ _
-        _ ≤ min (min (δ / 2) r) (B (n + 1)) + δ / 2 := (add_le_add hz (le_of_lt xy))
-        _ ≤ δ / 2 + δ / 2 := (add_le_add (le_trans (min_le_left _ _) (min_le_left _ _)) le_rfl)
-        _ = δ := ENNReal.add_halves δ
-    show z ∈ f n
-    exact hr (calc
-      edist z y ≤ min (min (δ / 2) r) (B (n + 1)) := hz
-      _ ≤ r := le_trans (min_le_left _ _) (min_le_right _ _))
-  choose! center radius Hpos HB Hball using this
-  refine' fun x => (mem_closure_iff_nhds_basis nhds_basis_closed_eball).2 fun ε εpos => _
-  /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x` belonging to all
-    `f n`. For this, we construct inductively a sequence `F n = (c n, r n)` such that the closed
-    ball `closedBall (c n) (r n)` is included in the previous ball and in `f n`, and such that
-    `r n` is small enough to ensure that `c n` is a Cauchy sequence. Then `c n` converges to a
-    limit which belongs to all the `f n`. -/
-  let F : ℕ → X × ℝ≥0∞ := fun n =>
-    Nat.recOn n (Prod.mk x (min ε (B 0))) fun n p => Prod.mk (center n p.1 p.2) (radius n p.1 p.2)
-  let c : ℕ → X := fun n => (F n).1
-  let r : ℕ → ℝ≥0∞ := fun n => (F n).2
-  have rpos : ∀ n, 0 < r n := by
-    intro n
-    induction' n with n hn
-    exact lt_min εpos (Bpos 0)
-    exact Hpos n (c n) (r n) hn.ne'
-  have r0 : ∀ n, r n ≠ 0 := fun n => (rpos n).ne'
-  have rB : ∀ n, r n ≤ B n := by
-    intro n
-    induction' n with n _
-    exact min_le_right _ _
-    exact HB n (c n) (r n) (r0 n)
-  have incl : ∀ n, closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n :=
-    fun n => Hball n (c n) (r n) (r0 n)
-  have cdist : ∀ n, edist (c n) (c (n + 1)) ≤ B n := by
-    intro n
-    rw [edist_comm]
-    have A : c (n + 1) ∈ closedBall (c (n + 1)) (r (n + 1)) := mem_closedBall_self
-    have I :=
-      calc
-        closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) :=
-          Subset.trans (incl n) (inter_subset_left _ _)
-        _ ⊆ closedBall (c n) (B n) := closedBall_subset_closedBall (rB n)
-    exact I A
-  have : CauchySeq c := cauchySeq_of_edist_le_geometric_two _ one_ne_top cdist
-  -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`.
-  rcases cauchySeq_tendsto_of_complete this with ⟨y, ylim⟩
-  -- this point `y` will be the desired point. We will check that it belongs to all
-  -- `f n` and to `ball x ε`.
-  use y
-  simp only [exists_prop, Set.mem_iInter]
-  have I : ∀ n, ∀ m ≥ n, closedBall (c m) (r m) ⊆ closedBall (c n) (r n) := by
-    intro n
-    refine' Nat.le_induction _ fun m _ h => _
-    · exact Subset.refl _
-    · exact Subset.trans (incl m) (Subset.trans (inter_subset_left _ _) h)
-  have yball : ∀ n, y ∈ closedBall (c n) (r n) := by
-    intro n
-    refine' isClosed_ball.mem_of_tendsto ylim _
-    refine' (Filter.eventually_ge_atTop n).mono fun m hm => _
-    exact I n m hm mem_closedBall_self
-  constructor
-  show ∀ n, y ∈ f n
-  · intro n
-    have : closedBall (c (n + 1)) (r (n + 1)) ⊆ f n :=
-      Subset.trans (incl n) (inter_subset_right _ _)
-    exact this (yball (n + 1))
-  show edist y x ≤ ε
-  exact le_trans (yball 0) (min_le_left _ _)
-#align baire_category_theorem_emetric_complete BaireSpace.of_pseudoEMetricSpace_completeSpace
-
-/-- The second theorem states that locally compact R₁ spaces are Baire. -/
-instance (priority := 100) BaireSpace.of_t2Space_locallyCompactSpace
-    [TopologicalSpace X] [R1Space X] [LocallyCompactSpace X] : BaireSpace X := by
-  constructor
-  intro f ho hd
-  /- To prove that an intersection of open dense subsets is dense, prove that its intersection
-    with any open neighbourhood `U` is dense. Define recursively a decreasing sequence `K` of
-    compact neighbourhoods: start with some compact neighbourhood inside `U`, then at each step,
-    take its interior, intersect with `f n`, then choose a compact neighbourhood inside the
-    intersection. -/
-  rw [dense_iff_inter_open]
-  intro U U_open U_nonempty
-  -- Choose an antitone sequence of positive compacts such that `closure (K 0) ⊆ U`
-  -- and `closure (K (n + 1)) ⊆ f n` for all `n`
-  obtain ⟨K, hK_anti, hKf, hKU⟩ : ∃ K : ℕ → PositiveCompacts X,
-      (∀ n, K (n + 1) ≤ K n) ∧ (∀ n, closure ↑(K (n + 1)) ⊆ f n) ∧ closure ↑(K 0) ⊆ U := by
-    rcases U_open.exists_positiveCompacts_closure_subset U_nonempty with ⟨K₀, hK₀⟩
-    have : ∀ (n) (K : PositiveCompacts X),
-        ∃ K' : PositiveCompacts X, closure ↑K' ⊆ f n ∩ interior K := by
-      refine fun n K ↦ ((ho n).inter isOpen_interior).exists_positiveCompacts_closure_subset ?_
-      rw [inter_comm]
-      exact (hd n).inter_open_nonempty _ isOpen_interior K.interior_nonempty
-    choose K_next hK_next using this
-    refine ⟨Nat.rec K₀ K_next, fun n ↦ ?_, fun n ↦ (hK_next n _).trans (inter_subset_left _ _), hK₀⟩
-    exact subset_closure.trans <| (hK_next _ _).trans <|
-      (inter_subset_right _ _).trans interior_subset
-  -- Prove that ̀`⋂ n : ℕ, closure (K n)` is inside `U ∩ ⋂ n : ℕ, f n`.
-  have hK_subset : (⋂ n, closure (K n) : Set X) ⊆ U ∩ ⋂ n, f n := fun x hx ↦ by
-    simp only [mem_iInter, mem_inter_iff] at hx ⊢
-    exact ⟨hKU <| hx 0, fun n ↦ hKf n <| hx (n + 1)⟩
-  /- Prove that `⋂ n : ℕ, closure (K n)` is not empty, as an intersection of a decreasing sequence
-    of nonempty compact closed subsets. -/
-  have hK_nonempty : (⋂ n, closure (K n) : Set X).Nonempty :=
-    IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed _
-      (fun n => closure_mono <| hK_anti n) (fun n => (K n).nonempty.closure)
-      (K 0).isCompact.closure fun n => isClosed_closure
-  exact hK_nonempty.mono hK_subset
-#align baire_category_theorem_locally_compact BaireSpace.of_t2Space_locallyCompactSpace
-
 variable [TopologicalSpace X] [BaireSpace X]
 
 /-- Definition of a Baire space. -/