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.308407
s₂✝ : Finset ι₂
w : ι → k
p : ι → P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ ↑(affineCombination k s₁ p) w = ↑(affineCombination k s₂ p) (Set.indicator (↑s₁) w)
rw [affineCombination_apply, affineCombination_apply,
  weightedVSubOfPoint_indicator_subset _ _ _ h]