no goals
k : Type u_4
V : Type u_5
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type u_1
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
⊢ ↑(affineCombination k (map e s₂) p) w = ↑(affineCombination k s₂ (p ∘ ↑e)) (w ∘ ↑e)
simp_rw [affineCombination_apply, weightedVSubOfPoint_map]