no goals
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.365709
s₂ : Finset ι₂
w : ι → k
p : ι → P
pred : ι → Prop
inst✝ : DecidablePred pred
⊢ (↑(affineCombination k (Finset.subtype pred s) fun i => p ↑i) fun i => w ↑i) =
    ↑(affineCombination k (filter pred s) p) w
rw [affineCombination_apply, affineCombination_apply, weightedVSubOfPoint_subtype_eq_filter]