R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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 : P), p ∈ {x, y, z} → ∃ r, p = r • v +ᵥ p₀
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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}
rw [collinear_iff_exists_forall_eq_smul_vadd]
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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), p ∈ {x, y, z} → ∃ r, p = r • (z -ᵥ x) +ᵥ x
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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 : P), p ∈ {x, y, z} → ∃ r, p = r • v +ᵥ p₀
refine' ⟨x, z -ᵥ x, _⟩
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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), p ∈ {x, y, z} → ∃ r, p = r • (z -ᵥ x) +ᵥ x
intro p hp
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
simp_rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hp
case inl
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
rcases hp with (rfl | rfl | rfl)
case inl
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
case inl
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
refine' ⟨0, _⟩
no goals
case inl
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
simp
case inr.inl.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
case inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
rcases h with ⟨t, -, rfl⟩
no goals
case inr.inl.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
exact ⟨t, rfl⟩
case inr.inr
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
case inr.inr
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
refine' ⟨1, _⟩
no goals
case inr.inr
R : Type u_1
V : Type u_2
V' : Type ?u.589540
P : Type u_3
P' : Type ?u.589546
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
simp