k : Type u_2
V : Type ?u.444139
P : Type ?u.444142
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.444798
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ ∑ x in s, (c • weightedVSubVSubWeights k j i) x + ∑ x in s, affineCombinationSingleWeights k i x = 1
k : Type u_2
V : Type ?u.444139
P : Type ?u.444142
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.444798
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ ∑ t in s, affineCombinationLineMapWeights i j c t = 1
simp_rw [affineCombinationLineMapWeights, Pi.add_apply, sum_add_distrib]
no goals
k : Type u_2
V : Type ?u.444139
P : Type ?u.444142
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.444798
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ ∑ x in s, (c • weightedVSubVSubWeights k j i) x + ∑ x in s, affineCombinationSingleWeights k i x = 1
simp [hi, hj, ← mul_sum]