no goals
k : Type u_3
V : Type u_1
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.106184
s₂ : Finset ι₂
w : ι → k
p₂ : ι → P
p₁ b : P
⊢ ∑ i in s, w i • (p₁ -ᵥ p₂ i) = (∑ i in s, w i) • (p₁ -ᵥ b) - ↑(weightedVSubOfPoint s p₂ b) w
rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]