Theorem: SBtw.sbtw.asymm_right (LeanCamCombi/MetricBetween.lean)

State before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
⊢ False
Tactic:
have := h'.dist
State after:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this : Dist.dist v u + Dist.dist u x = Dist.dist v x
⊢ False

State before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this : Dist.dist v u + Dist.dist u x = Dist.dist v x
⊢ False
Tactic:
rw [dist_comm] at this
State after:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this : Dist.dist u v + Dist.dist u x = Dist.dist v x
⊢ False

State before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this : Dist.dist u v + Dist.dist u x = Dist.dist v x
⊢ False
Tactic:
have : Dist.dist u v = 0 := by linarith [h.dist]
State after:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this✝ : Dist.dist u v + Dist.dist u x = Dist.dist v x
this : Dist.dist u v = 0
⊢ False

State before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this✝ : Dist.dist u v + Dist.dist u x = Dist.dist v x
this : Dist.dist u v = 0
⊢ False
Tactic:
simp [h.ne12] at this
State after:
no goals

State before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this : Dist.dist u v + Dist.dist u x = Dist.dist v x
⊢ Dist.dist u v = 0
Tactic:
linarith [h.dist]
State after:
no goals