-- Mathlib/LinearAlgebra/Vandermonde.lean
theorem det_vandermonde {n : ℕ} (v : Fin n → R) :
    det (vandermonde v) = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)

Proof state:
case e_M.h.e_6.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : ∀ (v : Fin n → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n + 1) → R
⊢ (fun i j => vecCons (v 0 ^ ↑j.succ) (fun i => v i.succ ^ ↑j.succ - v 0 ^ ↑j.succ) (Fin.succAbove 0 i)) = fun i j =>
    (v i.succ - v 0) * ∑ k ∈ range (↑j + 1), v i.succ ^ k * v 0 ^ (↑j - k)

Tactic:
ext i j

Result:
case e_M.h.e_6.h.h.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : ∀ (v : Fin n → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n + 1) → R
i j : Fin n
⊢ vecCons (v 0 ^ ↑j.succ) (fun i => v i.succ ^ ↑j.succ - v 0 ^ ↑j.succ) (Fin.succAbove 0 i) =
    (v i.succ - v 0) * ∑ k ∈ range (↑j + 1), v i.succ ^ k * v 0 ^ (↑j - k)

Proof state:
case succ.calc_1.refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : ∀ (v : Fin n → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n + 1) → R
i✝ j : Fin n.succ
i : Fin n
⊢ v i.succ ^ ↑j = v i.succ ^ ↑j - v 0 ^ ↑j + 1 * v 0 ^ ↑j

Tactic:
ring

Result:
no goals

Proof state:
case succ.calc_1.refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : ∀ (v : Fin n → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n + 1) → R
i✝ j : Fin n.succ
i : Fin n
⊢ v i.succ ^ ↑j = vecCons (v 0 ^ ↑j) (fun i => v i.succ ^ ↑j - v 0 ^ ↑j) i.succ + vecCons 0 1 i.succ * v 0 ^ ↑j

Tactic:
rw [Matrix.cons_val_succ, Matrix.cons_val_succ, Pi.one_apply]

Result:
case succ.calc_1.refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : ∀ (v : Fin n → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n + 1) → R
i✝ j : Fin n.succ
i : Fin n
⊢ v i.succ ^ ↑j = v i.succ ^ ↑j - v 0 ^ ↑j + 1 * v 0 ^ ↑j

Proof state:
case succ.calc_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : ∀ (v : Fin n → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n + 1) → R
⊢ (det fun i j => ∑ k ∈ range (↑j + 1), v i.succ ^ k * v 0 ^ (↑j - k)) = (of fun i j => v i.succ ^ ↑j).det

Tactic:
cases n

Result:
case succ.calc_2.zero
R : Type u_1
inst✝ : CommRing R
ih : ∀ (v : Fin 0 → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin 0, ∏ j ∈ Ioi i, (v j - v i)
v : Fin (0 + 1) → R
⊢ (det fun i j => ∑ k ∈ range (↑j + 1), v i.succ ^ k * v 0 ^ (↑j - k)) = (of fun i j => v i.succ ^ ↑j).det

case succ.calc_2.succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
ih : ∀ (v : Fin (n✝ + 1) → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin (n✝ + 1), ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n✝ + 1 + 1) → R
⊢ (det fun i j => ∑ k ∈ range (↑j + 1), v i.succ ^ k * v 0 ^ (↑j - k)) = (of fun i j => v i.succ ^ ↑j).det

Proof state:
case succ.calc_2.succ.A_succ.e_a
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
ih : ∀ (v : Fin (n✝ + 1) → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin (n✝ + 1), ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n✝ + 1 + 1) → R
i : Fin (n✝ + 1)
j : Fin n✝
i' : ℕ
hi' : i' ∈ range (↑j + 1)
⊢ i' ≤ ↑j

Tactic:
exact Nat.lt_succ_iff.mp (Finset.mem_range.mp hi')

Result:
no goals

Proof state:
case succ.calc_2.succ.A_succ.e_a
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
ih : ∀ (v : Fin (n✝ + 1) → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin (n✝ + 1), ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n✝ + 1 + 1) → R
i : Fin (n✝ + 1)
j : Fin n✝
i' : ℕ
hi' : i' ∈ range (↑j + 1)
⊢ v i.succ ^ i' * v 0 ^ (↑j + 1 - i') = v 0 * (v i.succ ^ i' * v 0 ^ (↑j - i'))

Tactic:
rw [mul_left_comm (v 0), Nat.succ_sub, pow_succ']

Result:
case succ.calc_2.succ.A_succ.e_a
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
ih : ∀ (v : Fin (n✝ + 1) → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin (n✝ + 1), ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n✝ + 1 + 1) → R
i : Fin (n✝ + 1)
j : Fin n✝
i' : ℕ
hi' : i' ∈ range (↑j + 1)
⊢ i' ≤ ↑j

Proof state:
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
ih : ∀ (v : Fin (n✝ + 1) → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin (n✝ + 1), ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n✝ + 1 + 1) → R
⊢ ∀ (i : Fin (n✝ + 1)) (j : Fin n✝),
    ∑ k ∈ range (↑j.succ + 1), v i.succ ^ k * v 0 ^ (↑j.succ - k) =
      of (fun i j => v i.succ ^ ↑j) i j.succ +
        v 0 * ∑ k ∈ range (↑j.castSucc + 1), v i.succ ^ k * v 0 ^ (↑j.castSucc - k)

Tactic:
intro i j

Result:
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
ih : ∀ (v : Fin (n✝ + 1) → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin (n✝ + 1), ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n✝ + 1 + 1) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ ∑ k ∈ range (↑j.succ + 1), v i.succ ^ k * v 0 ^ (↑j.succ - k) =
    of (fun i j => v i.succ ^ ↑j) i j.succ + v 0 * ∑ k ∈ range (↑j.castSucc + 1), v i.succ ^ k * v 0 ^ (↑j.castSucc - k)

Proof state:
case succ.calc_2.succ.A_zero
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
ih : ∀ (v : Fin (n✝ + 1) → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin (n✝ + 1), ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n✝ + 1 + 1) → R
⊢ ∀ (i : Fin (n✝ + 1)), ∑ k ∈ range (↑0 + 1), v i.succ ^ k * v 0 ^ (↑0 - k) = of (fun i j => v i.succ ^ ↑j) i 0

Tactic:
intro j

Result:
case succ.calc_2.succ.A_zero
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
ih : ∀ (v : Fin (n✝ + 1) → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin (n✝ + 1), ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n✝ + 1 + 1) → R
j : Fin (n✝ + 1)
⊢ ∑ k ∈ range (↑0 + 1), v j.succ ^ k * v 0 ^ (↑0 - k) = of (fun i j => v i.succ ^ ↑j) j 0

Proof state:
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
ih : ∀ (v : Fin (n✝ + 1) → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin (n✝ + 1), ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n✝ + 1 + 1) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ ∑ k ∈ range (↑j.succ + 1), v i.succ ^ k * v 0 ^ (↑j.succ - k) =
    of (fun i j => v i.succ ^ ↑j) i j.succ + v 0 * ∑ k ∈ range (↑j.castSucc + 1), v i.succ ^ k * v 0 ^ (↑j.castSucc - k)

Tactic:
simp only [smul_eq_mul, Pi.add_apply, Fin.val_succ, Fin.coe_castSucc, Pi.smul_apply]

Result:
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
ih : ∀ (v : Fin (n✝ + 1) → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin (n✝ + 1), ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n✝ + 1 + 1) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ ∑ x ∈ range (↑j + 1 + 1), v i.succ ^ x * v 0 ^ (↑j + 1 - x) =
    of (fun i j => v i.succ ^ ↑j) i j.succ + v 0 * ∑ x ∈ range (↑j + 1), v i.succ ^ x * v 0 ^ (↑j - x)

Proof state:
case succ.calc_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : ∀ (v : Fin n → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n + 1) → R
⊢ ∀ (i j : Fin n.succ),
    of (fun i j => v i ^ ↑j) i j =
      of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v i.succ ^ ↑j - v 0 ^ ↑j) i) i j +
        vecCons 0 1 i * of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v i.succ ^ ↑j - v 0 ^ ↑j) i) 0 j

Tactic:
intro i j

Result:
case succ.calc_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : ∀ (v : Fin n → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n + 1) → R
i j : Fin n.succ
⊢ of (fun i j => v i ^ ↑j) i j =
    of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v i.succ ^ ↑j - v 0 ^ ↑j) i) i j +
      vecCons 0 1 i * of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v i.succ ^ ↑j - v 0 ^ ↑j) i) 0 j

Proof state:
case e_M.h.e_6.h.h.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : ∀ (v : Fin n → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n + 1) → R
i j : Fin n
⊢ vecCons (v 0 ^ ↑j.succ) (fun i => v i.succ ^ ↑j.succ - v 0 ^ ↑j.succ) (Fin.succAbove 0 i) =
    (v i.succ - v 0) * ∑ k ∈ range (↑j + 1), v i.succ ^ k * v 0 ^ (↑j - k)

Tactic:
rw [Fin.succAbove_zero, Matrix.cons_val_succ, Fin.val_succ, mul_comm]

Result:
case e_M.h.e_6.h.h.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : ∀ (v : Fin n → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n + 1) → R
i j : Fin n
⊢ v i.succ ^ (↑j + 1) - v 0 ^ (↑j + 1) = (∑ k ∈ range (↑j + 1), v i.succ ^ k * v 0 ^ (↑j - k)) * (v i.succ - v 0)