chore: move IsOpenQuotientMap.baireSpace to Baire.Lemmas (leanprover-community#40713)

This makes the import tree a bit cleaner, so that importing `OpenQuotient` is cheaper.

Author: ADedecker

Mathlib/Topology/Baire/Lemmas.lean

@@ -6,8 +6,9 @@ Authors: Sébastien Gouëzel
 module
 
 public import Mathlib.Data.Fintype.Powerset
-public import Mathlib.Topology.GDelta.Basic
 public import Mathlib.Topology.Constructions
+public import Mathlib.Topology.GDelta.Basic
+public import Mathlib.Topology.Maps.OpenQuotient
 public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
@@ -111,6 +112,15 @@ theorem Topology.IsOpenEmbedding.baireSpace {Y : Type*} [TopologicalSpace Y] {p
 theorem IsOpen.baireSpace {s : Set X} (hO : IsOpen s) : BaireSpace s :=
   hO.isOpenEmbedding_subtypeVal.baireSpace
 
+/-- If `f` is an open quotient map and `X` is Baire, then `Y` is Baire. -/
+theorem IsOpenQuotientMap.baireSpace {Y : Type*} [TopologicalSpace Y] {f : X → Y}
+    (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]
+
 /-- 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

@@ -9,6 +9,7 @@ public import Mathlib.Logic.Equiv.Fin.Basic
 public import Mathlib.Topology.Connected.LocallyConnected
 public import Mathlib.Topology.DenseEmbedding
 public import Mathlib.Topology.Connected.TotallyDisconnected
+public import Mathlib.Topology.Baire.Lemmas
 
 /-!
 # Further properties of homeomorphisms

Mathlib/Topology/Maps/OpenQuotient.lean

@@ -6,7 +6,6 @@ Authors: Yury Kudryashov
 module
 
 public import Mathlib.Topology.Maps.Basic
-public import Mathlib.Topology.Baire.Lemmas
 
 /-!
 # Open quotient maps
@@ -65,15 +64,6 @@ 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)

Mathlib/Topology/Order/IsLUB.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 -/
 module
 
+public import Mathlib.Order.Filter.CountableInter
 public import Mathlib.Topology.Order.LeftRightNhds
 
 /-!