no goals
k : Type u_3
V : Type u_2
P : Type u_1
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type ?u.284656
inst✝¹ : DecidableEq P
inst✝ : DecidableEq V
s : Finset P
p : P
hp : p ∈ s
⊢ vectorSpan k ↑s = Submodule.span k ↑(Finset.image (fun x => x -ᵥ p) (Finset.erase s p))
simp [vectorSpan_eq_span_vsub_set_right_ne _ (Finset.mem_coe.mpr hp)]