no goals
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
j : ι
hj : j ∈ s
⊢ ↑C (r j) * Lagrange.basis s v j = ↑C (nodalWeight s v j) * (nodal s v / (X - ↑C (v j))) * ↑C (r j)
rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hj]