case h.dist.h.h
α✝ : Type u
β : Type v
X : Type ?u.563888
ι : Type ?u.563891
inst✝¹ : PseudoMetricSpace α✝
γ : Type w
inst✝ : MetricSpace γ
α : Type u_1
m : MetricSpace α
B : Bornology α
H : ∀ (s : Set α), IsBounded s ↔ IsBounded s
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
α✝ : Type u
β : Type v
X : Type ?u.563888
ι : Type ?u.563891
inst✝¹ : PseudoMetricSpace α✝
γ : Type w
inst✝ : MetricSpace γ
α : Type u_1
m : MetricSpace α
B : Bornology α
H : ∀ (s : Set α), IsBounded s ↔ IsBounded s
⊢ replaceBornology m H = m
ext
no goals
case h.dist.h.h
α✝ : Type u
β : Type v
X : Type ?u.563888
ι : Type ?u.563891
inst✝¹ : PseudoMetricSpace α✝
γ : Type w
inst✝ : MetricSpace γ
α : Type u_1
m : MetricSpace α
B : Bornology α
H : ∀ (s : Set α), IsBounded s ↔ IsBounded s
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
rfl