k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
⊢ ↑(affineCombination k s p) w = p i
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
⊢ ↑(affineCombination k s p) w = p i
have h1 : (∑ i in s, w i) = 1 := hwi ▸ sum_eq_single i hw0 fun h => False.elim (h his)
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
⊢ ∑ i_1 in s, w i_1 • (p i_1 -ᵥ p i) +ᵥ p i = p i
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
⊢ ↑(affineCombination k s p) w = p i
rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p h1 (p i),
  weightedVSubOfPoint_apply]
case h.e'_2.h.e'_5
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
⊢ ∑ i_1 in s, w i_1 • (p i_1 -ᵥ p i) = 0
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
⊢ ∑ i_1 in s, w i_1 • (p i_1 -ᵥ p i) +ᵥ p i = p i
convert zero_vadd V (p i)
case h.e'_2.h.e'_5
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
⊢ ∀ (x : ι), x ∈ s → w x • (p x -ᵥ p i) = 0
case h.e'_2.h.e'_5
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
⊢ ∑ i_1 in s, w i_1 • (p i_1 -ᵥ p i) = 0
refine sum_eq_zero ?_
case h.e'_2.h.e'_5
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
i2 : ι
hi2 : i2 ∈ s
⊢ w i2 • (p i2 -ᵥ p i) = 0
case h.e'_2.h.e'_5
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
⊢ ∀ (x : ι), x ∈ s → w x • (p x -ᵥ p i) = 0
intro i2 hi2
case pos
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
i2 : ι
hi2 : i2 ∈ s
h : i2 = i
⊢ w i2 • (p i2 -ᵥ p i) = 0

case neg
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
i2 : ι
hi2 : i2 ∈ s
h : ¬i2 = i
⊢ w i2 • (p i2 -ᵥ p i) = 0
case h.e'_2.h.e'_5
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
i2 : ι
hi2 : i2 ∈ s
⊢ w i2 • (p i2 -ᵥ p i) = 0
by_cases h : i2 = i
no goals
case pos
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
i2 : ι
hi2 : i2 ∈ s
h : i2 = i
⊢ w i2 • (p i2 -ᵥ p i) = 0
simp [h]
no goals
case neg
k : Type u_2
V : Type u_4
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.299390
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
i2 : ι
hi2 : i2 ∈ s
h : ¬i2 = i
⊢ w i2 • (p i2 -ᵥ p i) = 0
simp [hw0 i2 hi2 h]