case a.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i j : Fin (n + 1)
⊢ vandermonde (Fin.cons v0 v) i j =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) i j
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
⊢ vandermonde (Fin.cons v0 v) = Fin.cons (fun j => v0 ^ ↑j) fun i => Fin.cons 1 fun j => v i * vandermonde v i j
ext (i j)
case a.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j : Fin (n + 1)
i : Fin n
⊢ vandermonde (Fin.cons v0 v) (Fin.succ i) j =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) (Fin.succ i) j
case a.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i j : Fin (n + 1)
⊢ vandermonde (Fin.cons v0 v) i j =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) i j
refine' Fin.cases (by simp) (fun i => _) i
case a.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j✝ : Fin (n + 1)
i j : Fin n
⊢ vandermonde (Fin.cons v0 v) (Fin.succ i) (Fin.succ j) =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) (Fin.succ i) (Fin.succ j)
case a.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j : Fin (n + 1)
i : Fin n
⊢ vandermonde (Fin.cons v0 v) (Fin.succ i) j =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) (Fin.succ i) j
refine' Fin.cases (by simp) (fun j => _) j
no goals
case a.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j✝ : Fin (n + 1)
i j : Fin n
⊢ vandermonde (Fin.cons v0 v) (Fin.succ i) (Fin.succ j) =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) (Fin.succ i) (Fin.succ j)
simp [pow_succ]
no goals
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i j : Fin (n + 1)
⊢ vandermonde (Fin.cons v0 v) 0 j =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) 0 j
simp
no goals
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j : Fin (n + 1)
i : Fin n
⊢ vandermonde (Fin.cons v0 v) (Fin.succ i) 0 =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) (Fin.succ i) 0
simp