no goals
k : Type u_2
V : Type u_4
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.369441
s₂ : Finset ι₂
w : ι → k
p : ι → P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
⊢ ↑(affineCombination k (filter pred s) p) w = ↑(affineCombination k s p) w
rw [affineCombination_apply, affineCombination_apply,
  s.weightedVSubOfPoint_filter_of_ne _ _ _ h]