α : Type u
β : Type v
X : Type ?u.6274
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z = edist y z
α : Type u
β : Type v
X : Type ?u.6274
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist z x = edist z y
rw [edist_comm z x, edist_comm z y]
no goals
α : Type u
β : Type v
X : Type ?u.6274
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z = edist y z
apply edist_congr_right h