no goals
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
⊢ ↑(interpolate {i} v) r = ↑C (r i)
rw [interpolate_apply, sum_singleton, basis_singleton, mul_one]