no goals
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.494322
p : P
ps : Set P
h : p ∈ affineSpan k ps
⊢ vectorSpan k (insert p ps) = vectorSpan k ps
simp_rw [← direction_affineSpan, affineSpan_insert_eq_affineSpan _ h]