no goals
k : Type u_2
V : Type u_1
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_3
s : Finset ι
ι₂ : Type ?u.134871
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
c : k
⊢ ↑(weightedVSubOfPoint s p b) (c • w) = c • ↑(weightedVSubOfPoint s p b) w
simp_rw [weightedVSubOfPoint_apply, smul_sum, Pi.smul_apply, smul_smul, smul_eq_mul]