no goals
k : Type u_3
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.453666
s₂ : Finset ι₂
inst✝ : DecidableEq ι
p : ι → P
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ↑(weightedVSub s p) (weightedVSubVSubWeights k i j) = p i -ᵥ p j
rw [weightedVSubVSubWeights, ← affineCombination_vsub,
  s.affineCombination_affineCombinationSingleWeights k p hi,
  s.affineCombination_affineCombinationSingleWeights k p hj]