feat: an open subset of a Baire space is Baire (leanprover-community#32673)

This PR proves the following lemmas:
1. If `f : X →  Y` is an open quotient map and `X` is a Baire space, then `Y` is Baire. As a corollary, a homeomorphism maps a Baire space to a Baire space.
3. If `f : X →  Y` is an open embedding and `Y` is a Baire space, then `X` is Baire. As a corollary, any open subset of a Baire space is Baire.

Formalized with help from Aristotle.

Author: CoolRmal

Mathlib/Topology/Baire/Lemmas.lean

@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel
 module
 
 public import Mathlib.Topology.GDelta.Basic
+public import Mathlib.Topology.Constructions
 
 /-!
 # Baire spaces
@@ -17,7 +18,7 @@ and all locally compact regular spaces are Baire spaces.
 We prove the theorems in `Mathlib/Topology/Baire/CompleteMetrizable`
 and `Mathlib/Topology/Baire/LocallyCompactRegular`.
 
-In this file we prove various corollaries of Baire theorems.
+In this file we prove some lemmas about Baire spaces.
 
 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
@@ -47,6 +48,39 @@ theorem dense_iInter_of_isOpen_nat {f : ℕ → Set X} (ho : ∀ n, IsOpen (f n)
     (hd : ∀ n, Dense (f n)) : Dense (⋂ n, f n) :=
   BaireSpace.baire_property f ho hd
 
+/-- If `p : Y → X` is an open embedding and `X` is a Baire space, then `Y` is a Baire space. -/
+theorem Topology.IsOpenEmbedding.baireSpace {Y : Type*} [TopologicalSpace Y] {p : Y → X}
+    (hp : Topology.IsOpenEmbedding p) : BaireSpace Y := by
+  constructor
+  intro f hof hdf
+  let s := range p
+  let c := fun n : ℕ => p '' f n ∪ (closure s)ᶜ
+  have c_open (n : ℕ) : IsOpen (c n) := IsOpen.union (hp.isOpenMap (f n) (hof n))
+    isClosed_closure.isOpen_compl
+  have c_dense (n : ℕ) : Dense (c n) := by
+    rw [dense_iff_closure_eq, subset_antisymm_iff]
+    have : univ ⊆ closure (c n) := calc
+      _ ⊆ (interior (closure s)) ∪ (interior (closure s))ᶜ := by grind
+      _ ⊆ closure s ∪ (interior (closure s))ᶜ := by gcongr; exact interior_subset
+      _ ⊆ closure (p '' f n) ∪ (interior (closure s))ᶜ := union_subset_union
+          (closure_minimal (hp.continuous.range_subset_closure_image_dense (hdf n))
+          isClosed_closure) (subset_refl (interior (closure s))ᶜ)
+      _ ⊆ closure (p '' f n) ∪ closure ((closure s)ᶜ) := union_subset_union (by simp) (by simp)
+      _ = closure (c n) := closure_union.symm
+    grind
+  have c_inter_dense : Dense (⋂ n, c n) := dense_iInter_of_isOpen_nat c_open c_dense
+  have c_inter_eq : ⋂ n, f n = p ⁻¹' (⋂ n, c n) := by
+    ext x
+    simp only [mem_iInter, mem_preimage, mem_union, mem_compl_iff, c]
+    refine ⟨fun h i => by grind, fun h i => ?_⟩
+    exact hp.injective.mem_set_image.mp (imp_iff_or_not.mpr (h i)
+      (subset_closure (mem_range_self x)))
+  exact c_inter_eq ▸ Dense.preimage c_inter_dense hp.isOpenMap
+
+/-- An open subset of a Baire space is Baire. -/
+theorem IsOpen.baireSpace {s : Set X} (hO : IsOpen s) : BaireSpace s :=
+  hO.isOpenEmbedding_subtypeVal.baireSpace
+
 /-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with ⋂₀. -/
 theorem dense_sInter_of_isOpen {S : Set (Set X)} (ho : ∀ s ∈ S, IsOpen s) (hS : S.Countable)
     (hd : ∀ s ∈ S, Dense s) : Dense (⋂₀ S) := by

Mathlib/Topology/Homeomorph/Lemmas.lean

@@ -37,6 +37,9 @@ protected theorem secondCountableTopology [SecondCountableTopology Y]
     (h : X ≃ₜ Y) : SecondCountableTopology X :=
   h.isInducing.secondCountableTopology
 
+protected theorem baireSpace [BaireSpace X] (f : X ≃ₜ Y) : BaireSpace Y :=
+  f.isOpenQuotientMap.baireSpace
+
 /-- If `h : X → Y` is a homeomorphism, `h(s)` is compact iff `s` is. -/
 @[simp]
 theorem isCompact_image {s : Set X} (h : X ≃ₜ Y) : IsCompact (h '' s) ↔ IsCompact s :=

Mathlib/Topology/Maps/OpenQuotient.lean

@@ -6,6 +6,7 @@ Authors: Yury Kudryashov
 module
 
 public import Mathlib.Topology.Maps.Basic
+public import Mathlib.Topology.Baire.Lemmas
 
 /-!
 # Open quotient maps
@@ -64,6 +65,15 @@ theorem dense_preimage_iff (h : IsOpenQuotientMap f) {s : Set Y} : Dense (f ⁻
   ⟨fun hs ↦ h.surjective.denseRange.dense_of_mapsTo h.continuous hs (mapsTo_preimage _ _),
     fun hs ↦ hs.preimage h.isOpenMap⟩
 
+/-- If `f` is an open quotient map and `X` is Baire, then `Y` is Baire. -/
+theorem baireSpace {f : X → Y} [BaireSpace X] (hf : IsOpenQuotientMap f) :
+    BaireSpace Y := by
+  constructor
+  intro u hou hdu
+  have := dense_iInter_of_isOpen_nat (fun n => hf.continuous.isOpen_preimage (u n) (hou n))
+    (fun n => (IsOpenQuotientMap.dense_preimage_iff hf).mpr (hdu n))
+  simp_all [← preimage_iInter, IsOpenQuotientMap.dense_preimage_iff]
+
 end IsOpenQuotientMap
 
 theorem Topology.IsInducing.isOpenQuotientMap_of_surjective (ind : IsInducing f)