k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
⊢ ∃ p₀ v, ∀ (p : P), p ∈ {p₁, p₂} → ∃ r, p = r • v +ᵥ p₀
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
⊢ Collinear k {p₁, p₂}
rw [collinear_iff_exists_forall_eq_smul_vadd]
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
⊢ ∀ (p : P), p ∈ {p₁, p₂} → ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
⊢ ∃ p₀ v, ∀ (p : P), p ∈ {p₁, p₂} → ∃ r, p = r • v +ᵥ p₀
use p₁, p₂ -ᵥ p₁
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p ∈ {p₁, p₂}
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
⊢ ∀ (p : P), p ∈ {p₁, p₂} → ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
intro p hp
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₁ ∨ p = p₂
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p ∈ {p₁, p₂}
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hp
case inl
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₁
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁

case inr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₂
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₁ ∨ p = p₂
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
cases' hp with hp hp
case inl
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₁
⊢ p = 0 • (p₂ -ᵥ p₁) +ᵥ p₁
case inl
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₁
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
use 0
no goals
case inl
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₁
⊢ p = 0 • (p₂ -ᵥ p₁) +ᵥ p₁
simp [hp]
case inr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₂
⊢ p = 1 • (p₂ -ᵥ p₁) +ᵥ p₁
case inr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₂
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
use 1
no goals
case inr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.267878
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₂
⊢ p = 1 • (p₂ -ᵥ p₁) +ᵥ p₁
simp [hp]