case h.h
α : Type u
β : Type v
X : Type ?u.14808
ι : Type ?u.14811
inst✝ : PseudoMetricSpace α
x y : α
⊢ Function.swap dist x y = dist x y
α : Type u
β : Type v
X : Type ?u.14808
ι : Type ?u.14811
inst✝ : PseudoMetricSpace α
⊢ Function.swap dist = dist
funext x y
no goals
case h.h
α : Type u
β : Type v
X : Type ?u.14808
ι : Type ?u.14811
inst✝ : PseudoMetricSpace α
x y : α
⊢ Function.swap dist x y = dist x y
exact dist_comm _ _