Update CompleteMetrizable.lean

Author: CoolRmal

Mathlib/Topology/Baire/CompleteMetrizable.lean

@@ -4,8 +4,7 @@ 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.Tactic.Finiteness
-import Mathlib.Topology.Metrizable.Uniformity
+import Mathlib.Topology.Metrizable.CompletelyMetrizable
 
 /-!
 # First Baire theorem
@@ -15,17 +14,17 @@ Since `Mathlib` does not have the notion of a completely metrizable topological
 we state it for a complete uniform space with countably generated uniformity filter.
 -/
 
-open Filter EMetric Set
-open scoped Topology Uniformity ENNReal
+open EMetric Set TopologicalSpace
+open scoped ENNReal
 
-variable {X : Type*} [UniformSpace X] [CompleteSpace X] [(𝓤 X).IsCountablyGenerated]
+variable {X : Type*} [TopologicalSpace X] [IsCompletelyMetrizableSpace X]
 
 /-- **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
+  let _ := upgradeIsCompletelyMetrizable X
   refine ⟨fun f ho hd => ?_⟩
   let B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
   have Bpos : ∀ n, 0 < B n := fun n ↦