k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.322022
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
h : p₁ ∈ affineSpan k {p₂, p₃}
⊢ Collinear k {p₂, p₃}
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.322022
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
h : p₁ ∈ affineSpan k {p₂, p₃}
⊢ Collinear k {p₁, p₂, p₃}
rw [collinear_insert_iff_of_mem_affineSpan h]
no goals
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.322022
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
h : p₁ ∈ affineSpan k {p₂, p₃}
⊢ Collinear k {p₂, p₃}
exact collinear_pair _ _ _