F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hx : ∀ (i : ι), i ∈ s → x ≠ v i
⊢ ∑ x_1 in s, r x_1 * eval x (Lagrange.basis s v x_1) =
    ∑ x_1 in s, eval x (nodal s v) * (nodalWeight s v x_1 * (x - v x_1)⁻¹ * r x_1)
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hx : ∀ (i : ι), i ∈ s → x ≠ v i
⊢ eval x (↑(interpolate s v) r) = eval x (nodal s v) * ∑ i in s, nodalWeight s v i * (x - v i)⁻¹ * r i
simp_rw [interpolate_apply, mul_sum, eval_finset_sum, eval_mul, eval_C]
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i✝ : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hx : ∀ (i : ι), i ∈ s → x ≠ v i
i : ι
hi : i ∈ s
⊢ r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hx : ∀ (i : ι), i ∈ s → x ≠ v i
⊢ ∑ x_1 in s, r x_1 * eval x (Lagrange.basis s v x_1) =
    ∑ x_1 in s, eval x (nodal s v) * (nodalWeight s v x_1 * (x - v x_1)⁻¹ * r x_1)
refine' sum_congr rfl fun i hi => _
no goals
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i✝ : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hx : ∀ (i : ι), i ∈ s → x ≠ v i
i : ι
hi : i ∈ s
⊢ r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)
rw [← mul_assoc, mul_comm, eval_basis_not_at_node hi (hx _ hi)]