refine ⟨h12, ?_, h23, h.antisymm (dist_triangle _ _ _)⟩
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
⊢ sbtw u v w
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