no goals
k : Type u_2
V : Type u_3
P : Type ?u.282378
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι✝ : Type ?u.283028
s✝ : Finset ι✝
ι₂ : Type ?u.283034
s₂ : Finset ι₂
ι : Type u_1
s : Finset ι
w : ι → k
p : ι → V
hw : Finset.sum s w = 0
⊢ ↑(weightedVSub s p) w = ∑ i in s, w i • p i
simp [s.weightedVSub_apply, vsub_eq_sub, smul_sub, ← Finset.sum_smul, hw]