case h.dist.h.h
α : Type u
β : Type v
X : Type ?u.562313
ι : Type ?u.562316
inst✝¹ : PseudoMetricSpace α
γ✝ : Type w
inst✝ : MetricSpace γ✝
γ : Type u_1
U : UniformSpace γ
m : MetricSpace γ
H : 𝓤 γ = 𝓤 γ
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
α : Type u
β : Type v
X : Type ?u.562313
ι : Type ?u.562316
inst✝¹ : PseudoMetricSpace α
γ✝ : Type w
inst✝ : MetricSpace γ✝
γ : Type u_1
U : UniformSpace γ
m : MetricSpace γ
H : 𝓤 γ = 𝓤 γ
⊢ replaceUniformity m H = m
ext
no goals
case h.dist.h.h
α : Type u
β : Type v
X : Type ?u.562313
ι : Type ?u.562316
inst✝¹ : PseudoMetricSpace α
γ✝ : Type w
inst✝ : MetricSpace γ✝
γ : Type u_1
U : UniformSpace γ
m : MetricSpace γ
H : 𝓤 γ = 𝓤 γ
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
rfl