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.124383
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
⊢ (↑(weightedVSubOfPoint (Finset.subtype pred s) (fun i => p ↑i) b) fun i => w ↑i) =
    ↑(weightedVSubOfPoint (filter pred s) p b) w
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_subtype_eq_sum_filter]