case h.e'_2.h.e'_2.h.e'_2
α✝ : Type ?u.841
β : Type ?u.844
α : Type u_1
ht : TopologicalSpace α
h : PolishSpace α
⊢ polishSpaceMetric α = Exists.choose (_ : ∃ m, UniformSpace.toTopologicalSpace = ht ∧ CompleteSpace α)
α✝ : Type ?u.841
β : Type ?u.844
α : Type u_1
ht : TopologicalSpace α
h : PolishSpace α
⊢ CompleteSpace α
convert h.complete.choose_spec.2
no goals
case h.e'_2.h.e'_2.h.e'_2
α✝ : Type ?u.841
β : Type ?u.844
α : Type u_1
ht : TopologicalSpace α
h : PolishSpace α
⊢ polishSpaceMetric α = Exists.choose (_ : ∃ m, UniformSpace.toTopologicalSpace = ht ∧ CompleteSpace α)
exact MetricSpace.replaceTopology_eq _ _