no goals
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin (Nat.succ n) → R
⊢ vandermonde v =
    Fin.cons (fun j => v 0 ^ ↑j) fun i => Fin.cons 1 fun j => v (Fin.succ i) * vandermonde (Fin.tail v) i j
conv_lhs => rw [← Fin.cons_self_tail v, vandermonde_cons]