case h.dist.h.h
α : Type u
β : Type v
X : Type ?u.167309
ι : Type ?u.167312
inst✝ : PseudoMetricSpace α
γ : Type u_1
U : TopologicalSpace γ
m : PseudoMetricSpace γ
H : U = UniformSpace.toTopologicalSpace
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
α : Type u
β : Type v
X : Type ?u.167309
ι : Type ?u.167312
inst✝ : PseudoMetricSpace α
γ : Type u_1
U : TopologicalSpace γ
m : PseudoMetricSpace γ
H : U = UniformSpace.toTopologicalSpace
⊢ replaceTopology m H = m
ext
no goals
case h.dist.h.h
α : Type u
β : Type v
X : Type ?u.167309
ι : Type ?u.167312
inst✝ : PseudoMetricSpace α
γ : Type u_1
U : TopologicalSpace γ
m : PseudoMetricSpace γ
H : U = UniformSpace.toTopologicalSpace
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
rfl