Theorem: eqn_8 (LeanCamCombi/SylvesterChvatal.lean)

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
⊢ dist a b + dist b d < dist a d + Delta a b c
Tactic:
by_contra!
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
⊢ False

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
⊢ False
Tactic:
have hbcd : sbtw b c d := by
  refine sbtw_mk habc.2.1.ne hacd.ne23 ?_
  rw [Delta] at this
  linarith [hacd.dist]
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
hbcd : sbtw b c d
⊢ False

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
hbcd : sbtw b c d
⊢ False
Tactic:
refine habc.2.2.2.2.2.2 (Line c d) (Line_isLine hbcd.ne23) ?_
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
hbcd : sbtw b c d
⊢ {a, b, c} ⊆ Line c d

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
hbcd : sbtw b c d
⊢ {a, b, c} ⊆ Line c d
Tactic:
simp [left_extend_mem_Line, hacd, hbcd]
State after:
no goals

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
⊢ sbtw b c d
Tactic:
refine sbtw_mk habc.2.1.ne hacd.ne23 ?_
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
⊢ dist b c + dist c d ≤ dist b d

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
⊢ dist b c + dist c d ≤ dist b d
Tactic:
rw [Delta] at this
State after:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
this : dist a d + (dist a b + dist b c - dist a c) ≤ dist a b + dist b d
⊢ dist b c + dist c d ≤ dist b d

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
this : dist a d + (dist a b + dist b c - dist a c) ≤ dist a b + dist b d
⊢ dist b c + dist c d ≤ dist b d
Tactic:
linarith [hacd.dist]
State after:
no goals