Theorem: sbtw_mk (LeanCamCombi/MetricBetween.lean)

State before:
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
Tactic:
refine ⟨h12, ?_, h23, h.antisymm (dist_triangle _ _ _)⟩
State after:
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

State before:
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
Tactic:
rintro rfl
State after:
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

State before:
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
Tactic:
rw [dist_self] at h
State after:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : dist u v + dist v u ≤ 0
⊢ False

State before:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : dist u v + dist v u ≤ 0
⊢ False
Tactic:
replace h : dist v u ≤ 0 := by linarith [dist_comm v u]
State after:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : dist v u ≤ 0
⊢ False

State before:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : dist v u ≤ 0
⊢ False
Tactic:
simp only [dist_le_zero] at h
State after:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : v = u
⊢ False

State before:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : v = u
⊢ False
Tactic:
exact h23 h
State after:
no goals

State before:
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : dist u v + dist v u ≤ 0
⊢ dist v u ≤ 0
Tactic:
linarith [dist_comm v u]
State after:
no goals