no goals
k : Type u_1
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.344641
s₂ : Finset ι₂
w : ι → k
p₁ : ι → P
p₂ : P
h : ∑ i in s, w i = 1
⊢ ∑ i in s, w i • (p₁ i -ᵥ p₂) = ↑(affineCombination k s p₁) w -ᵥ p₂
rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]