no goals
k : Type u_3
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.111150
s₂✝ : Finset ι₂
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
⊢ ↑(weightedVSubOfPoint (s \ s₂) p b) w + ↑(weightedVSubOfPoint s₂ p b) w = ↑(weightedVSubOfPoint s p b) w
simp_rw [weightedVSubOfPoint_apply, sum_sdiff h]