no goals
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i✝ j : ι
v r r' : ι → F
hrr' : ∀ (i : ι), i ∈ s → r i = r' i
i : ι
hi : i ∈ s
⊢ ↑C (r i) * Lagrange.basis s v i = ↑C (r' i) * Lagrange.basis s v i
rw [hrr' _ hi]