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

Proof state:
case inr.inl.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
t : R
⊢ ∃ r, (lineMap x z) t = r • (z -ᵥ x) +ᵥ x

Tactic:
exact ⟨t, rfl⟩

Result:
no goals

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 : Wbtw R x y z
⊢ ∃ p₀ v, ∀ p ∈ {x, y, z}, ∃ r, p = r • v +ᵥ p₀

Tactic:
refine ⟨x, z -ᵥ x, ?_⟩

Result:
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 : Wbtw R x y z
⊢ ∀ p ∈ {x, y, z}, ∃ r, p = r • (z -ᵥ x) +ᵥ x

Proof state:
case 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
y z p : P
h : Wbtw R p y z
⊢ ∃ r, p = r • (z -ᵥ p) +ᵥ p

Tactic:
refine ⟨0, ?_⟩

Result:
case 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
y z p : P
h : Wbtw R p y z
⊢ p = 0 • (z -ᵥ p) +ᵥ p

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 : Wbtw R x y z
⊢ ∀ p ∈ {x, y, z}, ∃ r, p = r • (z -ᵥ x) +ᵥ x

Tactic:
intro p hp

Result:
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 : Wbtw R x y z
p : P
hp : p ∈ {x, y, z}
⊢ ∃ r, p = r • (z -ᵥ x) +ᵥ 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 : Wbtw R x y z
p : P
hp : p ∈ {x, y, z}
⊢ ∃ r, p = r • (z -ᵥ x) +ᵥ x

Tactic:
simp_rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hp

Result:
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 : Wbtw R x y z
p : P
hp : p = x ∨ p = y ∨ p = z
⊢ ∃ r, p = r • (z -ᵥ x) +ᵥ 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 : Wbtw R x y z
⊢ Collinear R {x, y, z}

Tactic:
rw [collinear_iff_exists_forall_eq_smul_vadd]

Result:
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 : Wbtw R x y z
⊢ ∃ p₀ v, ∀ p ∈ {x, y, z}, ∃ r, p = r • v +ᵥ p₀

Proof state:
case 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 y p : P
h : Wbtw R x y p
⊢ p = 1 • (p -ᵥ x) +ᵥ x

Tactic:
simp

Result:
no goals

Proof state:
case 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 y p : P
h : Wbtw R x y p
⊢ ∃ r, p = r • (p -ᵥ x) +ᵥ x

Tactic:
refine ⟨1, ?_⟩

Result:
case 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 y p : P
h : Wbtw R x y p
⊢ p = 1 • (p -ᵥ x) +ᵥ x

Proof state:
case 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 z p : P
h : Wbtw R x p z
⊢ ∃ r, p = r • (z -ᵥ x) +ᵥ x

Tactic:
rcases h with ⟨t, -, rfl⟩

Result:
case inr.inl.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
t : R
⊢ ∃ r, (lineMap x z) t = r • (z -ᵥ x) +ᵥ 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 : Wbtw R x y z
p : P
hp : p = x ∨ p = y ∨ p = z
⊢ ∃ r, p = r • (z -ᵥ x) +ᵥ x

Tactic:
rcases hp with (rfl | rfl | rfl)

Result:
case 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
y z p : P
h : Wbtw R p y z
⊢ ∃ r, p = r • (z -ᵥ p) +ᵥ p

case 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 z p : P
h : Wbtw R x p z
⊢ ∃ r, p = r • (z -ᵥ x) +ᵥ x

case 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 y p : P
h : Wbtw R x y p
⊢ ∃ r, p = r • (p -ᵥ x) +ᵥ x

Proof state:
case 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
y z p : P
h : Wbtw R p y z
⊢ p = 0 • (z -ᵥ p) +ᵥ p

Tactic:
simp

Result:
no goals