rintro rfl
V : Type u_1
inst✝ : MetricSpace V
u v w : V
h12 : u ≠ v
h23 : v ≠ w
h : dist u v + dist v w ≤ dist u w
⊢ u ≠ w
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : dist u v + dist v u ≤ dist u u
⊢ False