no goals
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.320461
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Collinear k (insert p s) ↔ Collinear k s
rw [Collinear, Collinear, vectorSpan_insert_eq_vectorSpan h]