no goals
k : Type u_3
V : Type u_1
P : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type ?u.264224
s₂ : Finset ι₂
w₁ w₂ : ι → k
p : ι → P
⊢ ↑(affineCombination k s p) w₁ -ᵥ ↑(affineCombination k s p) w₂ = ↑(weightedVSub s p) (w₁ - w₂)
rw [← AffineMap.linearMap_vsub, affineCombination_linear, vsub_eq_sub]