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.490167
p : P
ps : Set P
⊢ affineSpan k (insert p ↑(affineSpan k ps)) = affineSpan k (insert p ps)
rw [Set.insert_eq, Set.insert_eq, span_union, span_union, affineSpan_coe]