F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ eval (v i) (↑C (r i) * Lagrange.basis s v i) + ∑ x in Finset.erase s i, eval (v i) (↑C (r x) * Lagrange.basis s v x) =
    r i
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ eval (v i) (↑(interpolate s v) r) = r i
rw [interpolate_apply, eval_finset_sum, ← add_sum_erase _ _ hi]
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∑ x in Finset.erase s i, r x * eval (v i) (Lagrange.basis s v x) = 0
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ eval (v i) (↑C (r i) * Lagrange.basis s v i) + ∑ x in Finset.erase s i, eval (v i) (↑C (r x) * Lagrange.basis s v x) =
    r i
simp_rw [eval_mul, eval_C, eval_basis_self hvs hi, mul_one, add_right_eq_self]
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j✝ : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ Finset.erase s i
⊢ r j * eval (v i) (Lagrange.basis s v j) = 0
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∑ x in Finset.erase s i, r x * eval (v i) (Lagrange.basis s v x) = 0
refine' sum_eq_zero fun j H => _
no goals
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j✝ : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ Finset.erase s i
⊢ r j * eval (v i) (Lagrange.basis s v j) = 0
rw [eval_basis_of_ne (mem_erase.mp H).1 hi, MulZeroClass.mul_zero]