-- Mathlib/Analysis/Convex/Between.lean
theorem Collinear.wbtw_or_wbtw_or_wbtw {x y z : P} (h : Collinear R ({x, y, z} : Set P)) :
    Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y

Proof state:
case intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
tz : R
h : ∀ (p : P), p = x ∨ p = 0 • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x (0 • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (0 • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (0 • v +ᵥ x)

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : ty < 0
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Tactic:
rcases lt_trichotomy tz 0 with (hz0 | rfl | hz0)

Result:
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : ty < 0
hz0 : tz < 0
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

case intro.intro.intro.inl.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty : R
hy0 : ty < 0
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = 0 • v +ᵥ x → ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x (ty • v +ᵥ x) (0 • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (0 • v +ᵥ x) x ∨ Wbtw R (0 • v +ᵥ x) x (ty • v +ᵥ x)

case intro.intro.intro.inl.inr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : ty < 0
hz0 : 0 < tz
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Proof state:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
v : V
hz : ∃ r, z = r • v +ᵥ x
ty : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = z → ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x (ty • v +ᵥ x) z ∨ Wbtw R (ty • v +ᵥ x) z x ∨ Wbtw R z x (ty • v +ᵥ x)

Tactic:
rcases hz with ⟨tz, rfl⟩

Result:
case intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Proof state:
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : ty < 0
hz0 : tz < 0
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R x (tz • v +ᵥ x) (ty • v +ᵥ x) ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Tactic:
rw [← or_assoc]

Result:
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : ty < 0
hz0 : tz < 0
⊢ (Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R x (tz • v +ᵥ x) (ty • v +ᵥ x)) ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Proof state:
case intro.intro.intro.inr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : 0 < ty
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Tactic:
rcases lt_trichotomy tz 0 with (hz0 | rfl | hz0)

Result:
case intro.intro.intro.inr.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : 0 < ty
hz0 : tz < 0
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

case intro.intro.intro.inr.inr.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty : R
hy0 : 0 < ty
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = 0 • v +ᵥ x → ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x (ty • v +ᵥ x) (0 • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (0 • v +ᵥ x) x ∨ Wbtw R (0 • v +ᵥ x) x (ty • v +ᵥ x)

case intro.intro.intro.inr.inr.inr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : 0 < ty
hz0 : 0 < tz
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Proof state:
case intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
v : V
h : ∀ (p : P), p = x ∨ p = y ∨ p = z → ∃ r, p = r • v +ᵥ x
hy : ∃ r, y = r • v +ᵥ x
hz : ∃ r, z = r • v +ᵥ x
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y

Tactic:
rcases hy with ⟨ty, rfl⟩

Result:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
v : V
hz : ∃ r, z = r • v +ᵥ x
ty : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = z → ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x (ty • v +ᵥ x) z ∨ Wbtw R (ty • v +ᵥ x) z x ∨ Wbtw R z x (ty • v +ᵥ x)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : ∃ v, ∀ p ∈ {x, y, z}, ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y

Tactic:
rcases h with ⟨v, h⟩

Result:
case intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
v : V
h : ∀ p ∈ {x, y, z}, ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y

Proof state:
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : ty < 0
hz0 : tz < 0
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Tactic:
rw [wbtw_comm (z := x)]

Result:
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : ty < 0
hz0 : tz < 0
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R x (tz • v +ᵥ x) (ty • v +ᵥ x) ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)