k : Type u_2
V : Type ?u.415884
P : Type ?u.415887
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.416543
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i : ι
h : i ∈ s
⊢ ∑ j in s, affineCombinationSingleWeights k i j = affineCombinationSingleWeights k i i
k : Type u_2
V : Type ?u.415884
P : Type ?u.415887
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.416543
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i : ι
h : i ∈ s
⊢ ∑ j in s, affineCombinationSingleWeights k i j = 1
rw [← affineCombinationSingleWeights_apply_self k i]
no goals
k : Type u_2
V : Type ?u.415884
P : Type ?u.415887
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.416543
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i : ι
h : i ∈ s
⊢ ∑ j in s, affineCombinationSingleWeights k i j = affineCombinationSingleWeights k i i
exact sum_eq_single_of_mem i h fun j _ hj => affineCombinationSingleWeights_apply_of_ne k hj