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.457704
s₂ : Finset ι₂
inst✝ : DecidableEq ι
p : ι → P
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ ↑(affineCombination k s p) (affineCombinationLineMapWeights i j c) = ↑(AffineMap.lineMap (p i) (p j)) c
rw [affineCombinationLineMapWeights, ← weightedVSub_vadd_affineCombination,
  weightedVSub_const_smul, s.affineCombination_affineCombinationSingleWeights k p hi,
  s.weightedVSub_weightedVSubVSubWeights k p hj hi, AffineMap.lineMap_apply]