F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hi : i ∈ s
⊢ ∑ x in Finset.erase s i, eval (v i) (nodal (Finset.erase s x) v) = 0
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hi : i ∈ s
⊢ eval (v i) (↑derivative (nodal s v)) = eval (v i) (nodal (Finset.erase s i) v)
rw [derivative_nodal, eval_finset_sum, ← add_sum_erase _ _ hi, add_right_eq_self]
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hi : i ∈ s
j : ι
hj : j ∈ Finset.erase s i
⊢ eval (v i) (nodal (Finset.erase s j) v) = 0
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hi : i ∈ s
⊢ ∑ x in Finset.erase s i, eval (v i) (nodal (Finset.erase s x) v) = 0
refine' sum_eq_zero fun j hj => _
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hi : i ∈ s
j : ι
hj : j ∈ Finset.erase s i
⊢ ∃ a, (a ≠ j ∧ a ∈ s) ∧ v i - v a = 0
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hi : i ∈ s
j : ι
hj : j ∈ Finset.erase s i
⊢ eval (v i) (nodal (Finset.erase s j) v) = 0
simp_rw [nodal, eval_prod, eval_sub, eval_X, eval_C, prod_eq_zero_iff, mem_erase]
no goals
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hi : i ∈ s
j : ι
hj : j ∈ Finset.erase s i
⊢ ∃ a, (a ≠ j ∧ a ∈ s) ∧ v i - v a = 0
exact ⟨i, ⟨(mem_erase.mp hj).1.symm, hi⟩, sub_eq_zero_of_eq rfl⟩