no goals
k : Type u_1
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.247728
s₂ : Finset ι₂
w : ι → k
p : P
h : ∑ i in s, w i = 1
⊢ ↑(affineCombination k s fun x => p) w = p
rw [affineCombination_apply, s.weightedVSubOfPoint_apply_const, h, one_smul, vsub_vadd]