no goals
α : Type u
β : Type v
X : Type ?u.277189
ι : Type ?u.277192
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist (dist x y) (dist x z) ≤ dist y z
simpa only [dist_comm x] using dist_dist_dist_le_left y z x