-- 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:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
⊢ (vandermonde v).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)

Tactic:
unfold vandermonde

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
⊢ (of fun i j => v i ^ ↑j).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)

Proof state:
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
h : (of fun i j => v i.succ ^ ↑j).det = ∏ x : Fin n, ∏ y ∈ Ioi x, (v y.succ - v x.succ)
⊢ (∏ i : Fin n, (v i.succ - v 0)) * (of fun i j => v i.succ ^ ↑j).det =
    (∏ i : Fin n, (v i.succ - v 0)) * ∏ x : Fin n, ∏ j ∈ Ioi x, (v j.succ - v x.succ)

Tactic:
rw [h]

Result:
no goals

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
⊢ v i ^ ↑j =
    vecCons (v 0 ^ ↑j) (fun i => v i.succ ^ ↑j - v 0 ^ ↑j) i +
      vecCons 0 1 i * vecCons (v 0 ^ ↑j) (fun i => v i.succ ^ ↑j - v 0 ^ ↑j) 0

Tactic:
rw [Matrix.cons_val_zero]

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
⊢ v i ^ ↑j = vecCons (v 0 ^ ↑j) (fun i => v i.succ ^ ↑j - v 0 ^ ↑j) i + vecCons 0 1 i * v 0 ^ ↑j

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✝
⊢ ∑ x ∈ range (↑j + 1), v i.succ ^ x * v 0 ^ (↑j + 1 - x) =
    ∑ i_1 ∈ range (↑j + 1), v 0 * (v i.succ ^ i_1 * v 0 ^ (↑j - i_1))

Tactic:
refine Finset.sum_congr rfl fun i' hi' => ?_

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)
⊢ v i.succ ^ i' * v 0 ^ (↑j + 1 - i') = v 0 * (v i.succ ^ i' * v 0 ^ (↑j - i'))

Proof state:
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 : Fin n, (v i.succ - v 0)) * (of fun i j => v i.succ ^ ↑j).det =
    (∏ i : Fin n, (v i.succ - v 0)) * ∏ x : Fin n, ∏ j ∈ Ioi x, (v j.succ - v x.succ)

Tactic:
have h : (of fun i j : Fin n ↦ v i.succ ^ (j : ℕ)).det =
    ∏ x : Fin n, ∏ y ∈ Ioi x, (v y.succ - v x.succ) := by
  simpa using ih (v ∘ Fin.succ)

Result:
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
h : (of fun i j => v i.succ ^ ↑j).det = ∏ x : Fin n, ∏ y ∈ Ioi x, (v y.succ - v x.succ)
⊢ (∏ i : Fin n, (v i.succ - v 0)) * (of fun i j => v i.succ ^ ↑j).det =
    (∏ i : Fin n, (v i.succ - v 0)) * ∏ x : Fin n, ∏ j ∈ Ioi x, (v j.succ - v x.succ)

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
⊢ v i ^ ↑j = vecCons (v 0 ^ ↑j) (fun i => v i.succ ^ ↑j - v 0 ^ ↑j) i + vecCons 0 1 i * v 0 ^ ↑j

Tactic:
refine Fin.cases ?_ (fun i => ?_) i

Result:
case succ.calc_1.refine_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
⊢ v 0 ^ ↑j = vecCons (v 0 ^ ↑j) (fun i => v i.succ ^ ↑j - v 0 ^ ↑j) 0 + vecCons 0 1 0 * v 0 ^ ↑j

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

Proof state:
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 : Fin n, (v i.succ - v 0)) * (of fun i j => v i.succ ^ ↑j).det = ∏ i : Fin n.succ, ∏ j ∈ Ioi i, (v j - v i)

Tactic:
simp_rw [Fin.prod_univ_succ, Fin.prod_Ioi_zero, Fin.prod_Ioi_succ]

Result:
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 : Fin n, (v i.succ - v 0)) * (of fun i j => v i.succ ^ ↑j).det =
    (∏ i : Fin n, (v i.succ - v 0)) * ∏ x : Fin n, ∏ j ∈ Ioi x, (v j.succ - v x.succ)

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✝
⊢ ∑ 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)

Tactic:
rw [Finset.sum_range_succ, add_comm, tsub_self, pow_zero, mul_one, Finset.mul_sum]

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✝
⊢ v i.succ ^ (↑j + 1) + ∑ x ∈ range (↑j + 1), v i.succ ^ x * v 0 ^ (↑j + 1 - x) =
    of (fun i j => v i.succ ^ ↑j) i j.succ + ∑ i_1 ∈ range (↑j + 1), v 0 * (v i.succ ^ i_1 * v 0 ^ (↑j - i_1))

Proof state:
case succ.calc_1.refine_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
⊢ v 0 ^ ↑j = vecCons (v 0 ^ ↑j) (fun i => v i.succ ^ ↑j - v 0 ^ ↑j) 0 + vecCons 0 1 0 * v 0 ^ ↑j

Tactic:
simp

Result:
no goals

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
⊢ 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)

Tactic:
exact (geom_sum₂_mul (v i.succ) (v 0) (j + 1 : ℕ)).symm

Result:
no goals