no goals
k : Type u_2
V : Type u_3
P : Type ?u.291809
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s✝ : Finset ι
ι₂ : Type ?u.292465
s₂ : Finset ι₂
s : Finset ι
p : ι → V
w : ι → k
hw : ∑ i in s, w i = 1
⊢ ↑(affineCombination k s p) w = ∑ i in s, w i • p i
simp [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw 0]