Theorem: Delta_pos_of (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 u v w : V
h : NotCollinear u v w
⊢ 0 < Delta u v w
Tactic:
rw [Delta]
State after:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
⊢ 0 < dist u v + dist v w - dist u w

State before:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
⊢ 0 < dist u v + dist v w - dist u w
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 u v w : V
h : NotCollinear u v w
this : dist u v + dist v w - dist u w ≤ 0
⊢ False

State before:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
this : dist u v + dist v w - dist u w ≤ 0
⊢ False
Tactic:
have : sbtw u v w := sbtw_mk h.1 h.2.2.1 (by linarith only [this])
State after:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
this✝ : dist u v + dist v w - dist u w ≤ 0
this : sbtw u v w
⊢ False

State before:
V : Type u_1
inst✝² : MetricSpace V
u✝ v✝ w✝ : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z u v w : V
h : NotCollinear u v w
this✝ : dist u v + dist v w - dist u w ≤ 0
this : sbtw u v w
⊢ False
Tactic:
exact h.2.2.2 (Line u v) (Line_isLine this.ne12) (by simp [right_extend_mem_Line this])
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 u v w : V
h : NotCollinear u v w
this : dist u v + dist v w - dist u w ≤ 0
⊢ dist u v + dist v w ≤ dist u w
Tactic:
linarith only [this]
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 u v w : V
h : NotCollinear u v w
this✝ : dist u v + dist v w - dist u w ≤ 0
this : sbtw u v w
⊢ {u, v, w} ⊆ Line u v
Tactic:
simp [right_extend_mem_Line this]
State after:
no goals