refactor: have MetrizableSpace not depend on MetricSpace (#27946)

plp127 · urkud · plp127 · commit 6014a431eec4 · 2025-12-11T10:09:34.000Z
Some theorems for uniform spaces with a countably generated uniformity do not mention their uniformity in any of the hypotheses or the conclusion (for example `UniformSpace.isCompact_iff_isSeqCompact`). This PR allows those theorems to be stated for (pseudo)metrizable spaces without importing the real numbers. - Use `TopologicalSpace.pseudoMetrizableSpaceUniformity` to endow a pseudometrizable space with a compatible uniformity, and use `TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated` to show that this is countably generated. - `TopologicalSpace.pseudoMetrizableSpacePseudoMetric` and `TopologicalSpace.metrizableSpaceMetric` have been moved to `Mathlib/Topology/Metrizable/Uniformity.lean`. See also #2032 Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
diff --git a/Mathlib/Topology/Compactness/PseudometrizableLindelof.lean b/Mathlib/Topology/Compactness/PseudometrizableLindelof.lean
@@ -7,29 +7,6 @@ module
 
 public import Mathlib.Topology.Metrizable.Basic
 public import Mathlib.Topology.Compactness.Lindelof
+public import Mathlib.Tactic.Linter.DeprecatedModule
 
-/-!
-# Second-countability of pseudometrizable Lindelöf spaces
-
-Factored out from `Mathlib/Topology/Compactness/Lindelof.lean`
-to avoid circular dependencies.
--/
-
-@[expose] public section
-
-variable {X : Type*} [TopologicalSpace X]
-
-open Set Filter Topology TopologicalSpace
-
-instance SecondCountableTopology.ofPseudoMetrizableSpaceLindelofSpace [PseudoMetrizableSpace X]
-    [LindelofSpace X] : SecondCountableTopology X := by
-  letI : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
-  have h_dense (ε) (hpos : 0 < ε) : ∃ s : Set X, s.Countable ∧ ∀ x, ∃ y ∈ s, dist x y ≤ ε := by
-    let U := fun (z : X) ↦ Metric.ball z ε
-    obtain ⟨t, hct, huniv⟩ := LindelofSpace.elim_nhds_subcover U
-      (fun _ ↦ (Metric.isOpen_ball).mem_nhds (Metric.mem_ball_self hpos))
-    refine ⟨t, hct, fun z ↦ ?_⟩
-    obtain ⟨y, ht, hzy⟩ : ∃ y ∈ t, z ∈ U y :=
-      exists_set_mem_of_union_eq_top t (fun i ↦ U i) huniv z
-    exact ⟨y, ht, (Metric.mem_ball.mp hzy).le⟩
-  exact Metric.secondCountable_of_almost_dense_set h_dense
+deprecated_module (since := "2025-12-10")
diff --git a/Mathlib/Topology/GDelta/MetrizableSpace.lean b/Mathlib/Topology/GDelta/MetrizableSpace.lean
@@ -44,7 +44,8 @@ instance (priority := 100) [PseudoMetrizableSpace X] : NormalSpace X where
 
 instance (priority := 500) [PseudoMetrizableSpace X] : PerfectlyNormalSpace X where
   closed_gdelta s hs := by
-    let _ := pseudoMetrizableSpacePseudoMetric X
+    let := pseudoMetrizableSpaceUniformity X
+    have := pseudoMetrizableSpaceUniformity_countably_generated X
     rcases (@uniformity_hasBasis_open X _).exists_antitone_subbasis with ⟨U, hUo, hU, -⟩
     rw [← hs.closure_eq, ← hU.biInter_biUnion_ball]
     refine .biInter (to_countable _) fun n _ => IsOpen.isGδ ?_
@@ -61,7 +62,8 @@ variable {Y : Type*} [TopologicalSpace Y]
 
 theorem IsGδ.setOf_continuousAt [PseudoMetrizableSpace Y] (f : X → Y) :
     IsGδ { x | ContinuousAt f x } := by
-  let _ := pseudoMetrizableSpacePseudoMetric Y
+  let := pseudoMetrizableSpaceUniformity Y
+  have := pseudoMetrizableSpaceUniformity_countably_generated Y
   obtain ⟨U, _, hU⟩ := (@uniformity_hasBasis_open_symmetric Y _).exists_antitone_subbasis
   simp only [Uniform.continuousAt_iff_prod, nhds_prod_eq]
   simp only [(nhds_basis_opens _).prod_self.tendsto_iff hU.toHasBasis,
diff --git a/Mathlib/Topology/Metrizable/Basic.lean b/Mathlib/Topology/Metrizable/Basic.lean
@@ -5,129 +5,176 @@ Authors: Yury Kudryashov
 -/
 module
 
-public import Mathlib.Topology.MetricSpace.Basic
+public import Mathlib.Topology.UniformSpace.Pi
 
 /-!
-# Metrizability of a T₃ topological space with second countable topology
+# Metrizable Spaces
 
 In this file we define metrizable topological spaces, i.e., topological spaces for which there
 exists a metric space structure that generates the same topology.
+We define it without any reference to metric spaces in order to avoid importing the real numbers.
+For the proof that metrizable spaces admit a compatible metric,
+see `Mathlib/Topology/Metrizable/Uniformity`.
 -/
 
+-- don't import the real numbers
+assert_not_exists AddMonoidWithOne
+
 @[expose] public section
 
-open Filter Set Metric Topology
+open Filter Set Topology Uniformity
 
 namespace TopologicalSpace
 
 variable {ι X Y : Type*} {A : ι → Type*} [TopologicalSpace X] [TopologicalSpace Y] [Finite ι]
   [∀ i, TopologicalSpace (A i)]
 
 /-- A topological space is *pseudo metrizable* if there exists a pseudo metric space structure
-compatible with the topology. To endow such a space with a compatible distance, use
+compatible with the topology. To minimize imports, we implement this class in terms of the
+existence of a countably generated unifomity inducing the topology, which is mathematically
+equivalent.
+To endow such a space with a compatible uniformity, use
+`letI : UniformSpace X := TopologicalSpace.pseudoMetrizableSpaceUniformity X`.
+To endow such a space with a compatible distance, use
 `letI : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X`. -/
 class PseudoMetrizableSpace (X : Type*) [t : TopologicalSpace X] : Prop where
-  exists_pseudo_metric : ∃ m : PseudoMetricSpace X, m.toUniformSpace.toTopologicalSpace = t
-
-instance (priority := 100) _root_.PseudoMetricSpace.toPseudoMetrizableSpace {X : Type*}
-    [m : PseudoMetricSpace X] : PseudoMetrizableSpace X :=
-  ⟨⟨m, rfl⟩⟩
-
-/-- Construct on a metrizable space a metric compatible with the topology. -/
-noncomputable def pseudoMetrizableSpacePseudoMetric (X : Type*) [TopologicalSpace X]
-    [h : PseudoMetrizableSpace X] : PseudoMetricSpace X :=
-  h.exists_pseudo_metric.choose.replaceTopology h.exists_pseudo_metric.choose_spec.symm
+  exists_countably_generated :
+    ∃ u : UniformSpace X, u.toTopologicalSpace = t ∧ (uniformity X).IsCountablyGenerated
+
+/-- A uniform space with countably generated `𝓤 X` is pseudo metrizable. -/
+instance (priority := 100) _root_.UniformSpace.pseudoMetrizableSpace {X : Type*}
+    [u : UniformSpace X] [hu : IsCountablyGenerated (uniformity X)] : PseudoMetrizableSpace X :=
+  ⟨⟨u, rfl, hu⟩⟩
+
+/-- Construct on a pseudometrizable space a countably generated uniformity
+compatible with the topology. Use `pseudoMetrizableSpaceUniformity_countably_generated` for a proof
+that this uniformity is countably generated. -/
+-- see note [reducible non-instances]
+noncomputable abbrev pseudoMetrizableSpaceUniformity (X : Type*) [TopologicalSpace X]
+    [h : PseudoMetrizableSpace X] : UniformSpace X :=
+  h.exists_countably_generated.choose.replaceTopology
+    h.exists_countably_generated.choose_spec.1.symm
+
+example {X : Type*} [t : TopologicalSpace X] [PseudoMetrizableSpace X] :
+    (pseudoMetrizableSpaceUniformity X).toTopologicalSpace = t := by
+  with_reducible_and_instances rfl
+
+/-- The uniformity coming from `pseudoMetrizableSpaceUniformity` is countably generated.. -/
+theorem pseudoMetrizableSpaceUniformity_countably_generated
+    (X : Type*) [TopologicalSpace X] [h : PseudoMetrizableSpace X] :
+    𝓤[pseudoMetrizableSpaceUniformity X].IsCountablyGenerated :=
+  h.exists_countably_generated.choose_spec.2
 
 instance pseudoMetrizableSpace_prod [PseudoMetrizableSpace X] [PseudoMetrizableSpace Y] :
     PseudoMetrizableSpace (X × Y) :=
-  letI : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
-  letI : PseudoMetricSpace Y := pseudoMetrizableSpacePseudoMetric Y
+  let : UniformSpace X := pseudoMetrizableSpaceUniformity X
+  have : (uniformity X).IsCountablyGenerated :=
+    pseudoMetrizableSpaceUniformity_countably_generated X
+  let : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
+  have : (uniformity Y).IsCountablyGenerated :=
+    pseudoMetrizableSpaceUniformity_countably_generated Y
   inferInstance
 
 /-- Given an inducing map of a topological space into a pseudo metrizable space, the source space
 is also pseudo metrizable. -/
 theorem _root_.Topology.IsInducing.pseudoMetrizableSpace [PseudoMetrizableSpace Y] {f : X → Y}
     (hf : IsInducing f) : PseudoMetrizableSpace X :=
-  letI : PseudoMetricSpace Y := pseudoMetrizableSpacePseudoMetric Y
-  ⟨⟨hf.comapPseudoMetricSpace, rfl⟩⟩
+  let u : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
+  have : (uniformity Y).IsCountablyGenerated :=
+    pseudoMetrizableSpaceUniformity_countably_generated Y
+  ⟨⟨u.comap f, u.toTopologicalSpace_comap.trans hf.eq_induced.symm,
+    Filter.comap.isCountablyGenerated (uniformity Y) (Prod.map f f)⟩⟩
 
 /-- Every pseudo-metrizable space is first countable. -/
 instance (priority := 100) PseudoMetrizableSpace.firstCountableTopology
-    [h : PseudoMetrizableSpace X] : FirstCountableTopology X := by
-  rcases h with ⟨_, hm⟩
-  rw [← hm]
-  exact @UniformSpace.firstCountableTopology X PseudoMetricSpace.toUniformSpace
-    EMetric.instIsCountablyGeneratedUniformity
+    [h : PseudoMetrizableSpace X] : FirstCountableTopology X :=
+  let : UniformSpace X := pseudoMetrizableSpaceUniformity X
+  have : (uniformity X).IsCountablyGenerated :=
+    pseudoMetrizableSpaceUniformity_countably_generated X
+  inferInstance
 
 instance PseudoMetrizableSpace.subtype [PseudoMetrizableSpace X] (s : Set X) :
     PseudoMetrizableSpace s :=
   IsInducing.subtypeVal.pseudoMetrizableSpace
 
 instance pseudoMetrizableSpace_pi [∀ i, PseudoMetrizableSpace (A i)] :
-    PseudoMetrizableSpace (∀ i, A i) := by
-  cases nonempty_fintype ι
-  letI := fun i => pseudoMetrizableSpacePseudoMetric (A i)
-  infer_instance
+    PseudoMetrizableSpace (∀ i, A i) :=
+  let := fun i => pseudoMetrizableSpaceUniformity (A i)
+  have := fun i => pseudoMetrizableSpaceUniformity_countably_generated (A i)
+  inferInstance
+
+instance PseudoMetrizableSpace.regularSpace [PseudoMetrizableSpace X] : RegularSpace X :=
+  let := pseudoMetrizableSpaceUniformity X
+  inferInstance
 
 /-- A topological space is metrizable if there exists a metric space structure compatible with the
-topology. To endow such a space with a compatible distance, use
+topology. To minimize imports, we implement this class in terms of the existence of a
+countably generated unifomity inducing the topology, which is mathematically
+equivalent.
+To endow such a space with a compatible uniformity, use
+`letI : UniformSpace X := TopologicalSpace.pseudoMetrizableSpaceUniformity X`.
+To endow such a space with a compatible distance, use
 `letI : MetricSpace X := TopologicalSpace.metrizableSpaceMetric X`. -/
-class MetrizableSpace (X : Type*) [t : TopologicalSpace X] : Prop where
-  exists_metric : ∃ m : MetricSpace X, m.toUniformSpace.toTopologicalSpace = t
-
-instance (priority := 100) _root_.MetricSpace.toMetrizableSpace {X : Type*} [m : MetricSpace X] :
-    MetrizableSpace X :=
-  ⟨⟨m, rfl⟩⟩
+class MetrizableSpace (X : Type*) [t : TopologicalSpace X] : Prop extends
+    PseudoMetrizableSpace X, T0Space X
 
-instance (priority := 100) MetrizableSpace.toPseudoMetrizableSpace [h : MetrizableSpace X] :
-    PseudoMetrizableSpace X :=
-  let ⟨m, hm⟩ := h.1
-  ⟨⟨m.toPseudoMetricSpace, hm⟩⟩
+-- See note [lower instance priority]
+attribute [instance 100] MetrizableSpace.toT0Space
+attribute [instance 100] MetrizableSpace.toPseudoMetrizableSpace
 
 instance (priority := 100) PseudoMetrizableSpace.toMetrizableSpace
-    [T0Space X] [h : PseudoMetrizableSpace X] : MetrizableSpace X :=
-  letI := pseudoMetrizableSpacePseudoMetric X
-  ⟨.ofT0PseudoMetricSpace X, rfl⟩
-
-/-- Construct on a metrizable space a metric compatible with the topology. -/
-noncomputable def metrizableSpaceMetric (X : Type*) [TopologicalSpace X] [h : MetrizableSpace X] :
-    MetricSpace X :=
-  h.exists_metric.choose.replaceTopology h.exists_metric.choose_spec.symm
+    [T0Space X] [h : PseudoMetrizableSpace X] : MetrizableSpace X where
 
 instance (priority := 100) t2Space_of_metrizableSpace [MetrizableSpace X] : T2Space X :=
-  letI : MetricSpace X := metrizableSpaceMetric X
+  letI : UniformSpace X := pseudoMetrizableSpaceUniformity X
   inferInstance
 
-instance metrizableSpace_prod [MetrizableSpace X] [MetrizableSpace Y] : MetrizableSpace (X × Y) :=
-  letI : MetricSpace X := metrizableSpaceMetric X
-  letI : MetricSpace Y := metrizableSpaceMetric Y
-  inferInstance
+instance metrizableSpace_prod [MetrizableSpace X] [MetrizableSpace Y] :
+    MetrizableSpace (X × Y) where
 
 /-- Given an embedding of a topological space into a metrizable space, the source space is also
 metrizable. -/
 theorem _root_.Topology.IsEmbedding.metrizableSpace [MetrizableSpace Y] {f : X → Y}
-    (hf : IsEmbedding f) : MetrizableSpace X :=
-  letI : MetricSpace Y := metrizableSpaceMetric Y
-  ⟨⟨hf.comapMetricSpace f, rfl⟩⟩
+    (hf : IsEmbedding f) : MetrizableSpace X where
+  toPseudoMetrizableSpace := hf.toIsInducing.pseudoMetrizableSpace
+  toT0Space := hf.t0Space
 
 instance MetrizableSpace.subtype [MetrizableSpace X] (s : Set X) : MetrizableSpace s :=
   IsEmbedding.subtypeVal.metrizableSpace
 
-instance metrizableSpace_pi [∀ i, MetrizableSpace (A i)] : MetrizableSpace (∀ i, A i) := by
-  cases nonempty_fintype ι
-  letI := fun i => metrizableSpaceMetric (A i)
-  infer_instance
+instance metrizableSpace_pi [∀ i, MetrizableSpace (A i)] : MetrizableSpace (∀ i, A i) where
 
 theorem IsSeparable.secondCountableTopology [PseudoMetrizableSpace X] {s : Set X}
-    (hs : IsSeparable s) : SecondCountableTopology s := by
-  letI := pseudoMetrizableSpacePseudoMetric X
-  have := hs.separableSpace
-  exact UniformSpace.secondCountable_of_separable s
-
-instance (X : Type*) [TopologicalSpace X] [c : CompactSpace X] [MetrizableSpace X] :
+    (hs : IsSeparable s) : SecondCountableTopology s :=
+  let ⟨u, hu, hs⟩ := hs
+  have := hu.to_subtype
+  have : SeparableSpace (closure u) :=
+    ⟨Set.range (u.inclusion subset_closure), Set.countable_range (u.inclusion subset_closure),
+      Subtype.dense_iff.2 <| by rw [← Set.range_comp, Set.val_comp_inclusion, Subtype.range_coe]⟩
+  let := pseudoMetrizableSpaceUniformity (closure u)
+  have := pseudoMetrizableSpaceUniformity_countably_generated (closure u)
+  have := UniformSpace.secondCountable_of_separable (closure u)
+  (Topology.IsEmbedding.inclusion hs).secondCountableTopology
+
+instance (X : Type*) [TopologicalSpace X] [LindelofSpace X] [PseudoMetrizableSpace X] :
     SecondCountableTopology X := by
-  obtain ⟨_, h⟩ := MetrizableSpace.exists_metric (X := X)
-  rw [← h] at c ⊢
-  infer_instance
+  let := pseudoMetrizableSpaceUniformity X
+  have := pseudoMetrizableSpaceUniformity_countably_generated X
+  suffices _ : SeparableSpace X from UniformSpace.secondCountable_of_separable X
+  obtain ⟨V, hVb, hVs⟩ := UniformSpace.has_seq_basis X
+  choose U hUc hUu using fun n =>
+    LindelofSpace.elim_nhds_subcover (fun x => UniformSpace.ball x (V n))
+      (fun x => UniformSpace.ball_mem_nhds x (hVb.mem n))
+  refine ⟨Set.iUnion U, Set.countable_iUnion hUc, fun x => ?_⟩
+  rw [mem_closure_iff_frequently, nhds_eq_comap_uniformity, frequently_comap, hVb.frequently_iff]
+  intro n _
+  obtain ⟨i, hi, hx⟩ := Set.mem_iUnion₂.1 (Set.eq_univ_iff_forall.1 (hUu n) x)
+  rw [UniformSpace.ball_eq_of_symmetry] at hx
+  exact ⟨(x, i), hx, i, rfl, Set.mem_iUnion_of_mem n hi⟩
+
+instance (priority := 100) DiscreteTopology.metrizableSpace [DiscreteTopology X] :
+    MetrizableSpace X where
+  exists_countably_generated :=
+    ⟨⊥, DiscreteTopology.eq_bot.symm, Filter.isCountablyGenerated_principal SetRel.id⟩
 
 end TopologicalSpace
diff --git a/Mathlib/Topology/Metrizable/ContinuousMap.lean b/Mathlib/Topology/Metrizable/ContinuousMap.lean
@@ -26,11 +26,10 @@ variable {X Y : Type*}
   [TopologicalSpace Y]
 
 instance [PseudoMetrizableSpace Y] : PseudoMetrizableSpace C(X, Y) :=
-  let _ := pseudoMetrizableSpacePseudoMetric Y
+  let := pseudoMetrizableSpaceUniformity Y
+  have := pseudoMetrizableSpaceUniformity_countably_generated Y
   inferInstance
 
-instance [MetrizableSpace Y] : MetrizableSpace C(X, Y) :=
-  let _ := metrizableSpaceMetric Y
-  UniformSpace.metrizableSpace
+instance [MetrizableSpace Y] : MetrizableSpace C(X, Y) where
 
 end ContinuousMap
diff --git a/Mathlib/Topology/Metrizable/Real.lean b/Mathlib/Topology/Metrizable/Real.lean
@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 -/
 module
 
+public import Mathlib.Topology.MetricSpace.Basic
 public import Mathlib.Topology.Metrizable.Basic
 public import Mathlib.Topology.Order.MonotoneContinuity
 public import Mathlib.Topology.Order.Real
diff --git a/Mathlib/Topology/Metrizable/Uniformity.lean b/Mathlib/Topology/Metrizable/Uniformity.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Data.Nat.Lattice
 public import Mathlib.Data.NNReal.Basic
+public import Mathlib.Topology.MetricSpace.Basic
 public import Mathlib.Topology.Metrizable.Basic
 
 /-!
@@ -243,28 +244,44 @@ protected theorem UniformSpace.metrizable_uniformity (X : Type*) [UniformSpace X
       mul_one_div, div_le_iff₀ zero_lt_two, div_mul_cancel₀ _ two_ne_zero, hle_d]
 
 /-- A `PseudoMetricSpace` instance compatible with a given `UniformSpace` structure. -/
-protected noncomputable def UniformSpace.pseudoMetricSpace (X : Type*) [UniformSpace X]
+-- see note [reducible non-instances]
+protected noncomputable abbrev UniformSpace.pseudoMetricSpace (X : Type*) [UniformSpace X]
     [IsCountablyGenerated (𝓤 X)] : PseudoMetricSpace X :=
   (UniformSpace.metrizable_uniformity X).choose.replaceUniformity <|
     congr_arg _ (UniformSpace.metrizable_uniformity X).choose_spec.symm
 
 /-- A `MetricSpace` instance compatible with a given `UniformSpace` structure. -/
-protected noncomputable def UniformSpace.metricSpace (X : Type*) [UniformSpace X]
+-- see note [reducible non-instances]
+protected noncomputable abbrev UniformSpace.metricSpace (X : Type*) [UniformSpace X]
     [IsCountablyGenerated (𝓤 X)] [T0Space X] : MetricSpace X :=
   @MetricSpace.ofT0PseudoMetricSpace X (UniformSpace.pseudoMetricSpace X) _
 
-/-- A uniform space with countably generated `𝓤 X` is pseudo metrizable. -/
-instance (priority := 100) UniformSpace.pseudoMetrizableSpace [UniformSpace X]
-    [IsCountablyGenerated (𝓤 X)] : TopologicalSpace.PseudoMetrizableSpace X := by
-  letI := UniformSpace.pseudoMetricSpace X
-  infer_instance
-
 /-- A T₀ uniform space with countably generated `𝓤 X` is metrizable. This is not an instance to
 avoid loops. -/
 theorem UniformSpace.metrizableSpace [UniformSpace X] [IsCountablyGenerated (𝓤 X)] [T0Space X] :
-    TopologicalSpace.MetrizableSpace X := by
-  letI := UniformSpace.metricSpace X
-  infer_instance
+    TopologicalSpace.MetrizableSpace X := inferInstance
+
+/-- Construct on a pseudometrizable space a pseudometric compatible with the topology. -/
+-- see note [reducible non-instances]
+noncomputable abbrev TopologicalSpace.pseudoMetrizableSpacePseudoMetric (X : Type*)
+    [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] : PseudoMetricSpace X :=
+  letI := TopologicalSpace.pseudoMetrizableSpaceUniformity X
+  haveI := TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated X
+  UniformSpace.pseudoMetricSpace X
+
+example {X : Type*} [t : TopologicalSpace X] [t.PseudoMetrizableSpace] :
+    t.pseudoMetrizableSpacePseudoMetric.toUniformSpace = t.pseudoMetrizableSpaceUniformity := by
+  with_reducible_and_instances rfl
+
+/-- Construct on a metrizable space a metric compatible with the topology. -/
+noncomputable abbrev TopologicalSpace.metrizableSpaceMetric (X : Type*) [TopologicalSpace X]
+    [TopologicalSpace.MetrizableSpace X] : MetricSpace X :=
+  letI := pseudoMetrizableSpacePseudoMetric X
+  .ofT0PseudoMetricSpace X
+
+example {X : Type*} [t : TopologicalSpace X] [t.MetrizableSpace] :
+    t.metrizableSpaceMetric.toPseudoMetricSpace = t.pseudoMetrizableSpacePseudoMetric := by
+  with_reducible_and_instances rfl
 
 /-- A totally bounded set is separable in countably generated uniform spaces. This can be obtained
 from the more general `EMetric.subset_countable_closure_of_almost_dense_set`. -/
@@ -284,12 +301,6 @@ lemma TotallyBounded.isSeparable [UniformSpace X] [i : IsCountablyGenerated (
 variable {α : Type*}
 open TopologicalSpace
 
-instance (priority := 100) DiscreteTopology.metrizableSpace
-    [TopologicalSpace α] [DiscreteTopology α] :
-    MetrizableSpace α := by
-  obtain rfl := DiscreteTopology.eq_bot (α := α)
-  exact @UniformSpace.metrizableSpace α ⊥ (isCountablyGenerated_principal _) _
-
 instance (priority := 100) PseudoEMetricSpace.pseudoMetrizableSpace
     [PseudoEMetricSpace α] : PseudoMetrizableSpace α :=
   inferInstance
