α : Type u
β : Type v
X : Type ?u.9917
ι : Type ?u.9920
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist x z + dist z y
α : Type u
β : Type v
X : Type ?u.9917
ι : Type ?u.9920
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist x z + dist y z
rw [dist_comm y]
no goals
α : Type u
β : Type v
X : Type ?u.9917
ι : Type ?u.9920
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist x z + dist z y
apply dist_triangle