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

Tactic:
calc
  det (of fun i j : Fin n.succ => v i ^ (j : ℕ)) =
      det
        (of fun i j : Fin n.succ =>
          Matrix.vecCons (v 0 ^ (j : ℕ)) (fun i => v (Fin.succ i) ^ (j : ℕ) - v 0 ^ (j : ℕ)) i) :=
    det_eq_of_forall_row_eq_smul_add_const (Matrix.vecCons 0 1) 0 (Fin.cons_zero _ _) ?_
  _ =
      det
        (of fun i j : Fin n =>
          Matrix.vecCons (v 0 ^ (j.succ : ℕ))
            (fun i : Fin n => v (Fin.succ i) ^ (j.succ : ℕ) - v 0 ^ (j.succ : ℕ))
            (Fin.succAbove 0 i)) := by
    simp_rw [det_succ_column_zero, Fin.sum_univ_succ, of_apply, Matrix.cons_val_zero, submatrix,
      of_apply, Matrix.cons_val_succ, Fin.val_zero, pow_zero, one_mul, sub_self,
      mul_zero, zero_mul, Finset.sum_const_zero, add_zero]
  _ =
      det
        (of fun i j : Fin n =>
            (v (Fin.succ i) - v 0) *
              ∑ k ∈ Finset.range (j + 1 : ℕ), v i.succ ^ k * v 0 ^ (j - k : ℕ) :
          Matrix _ _ R) := by
    congr
    ext i j
    rw [Fin.succAbove_zero, Matrix.cons_val_succ, Fin.val_succ, mul_comm]
    exact (geom_sum₂_mul (v i.succ) (v 0) (j + 1 : ℕ)).symm
  _ =
      (∏ i ∈ Finset.univ, (v (Fin.succ i) - v 0)) *
        det fun i j : Fin n =>
          ∑ k ∈ Finset.range (j + 1 : ℕ), v i.succ ^ k * v 0 ^ (j - k : ℕ) :=
    (det_mul_column (fun i => v (Fin.succ i) - v 0) _)
  _ = (∏ i ∈ Finset.univ, (v (Fin.succ i) - v 0)) *
  det (of fun i j : Fin n => v (Fin.succ i) ^ (j : ℕ)) := congr_arg _ ?_
  _ = ∏ i : Fin n.succ, ∏ j ∈ Ioi i, (v j - v i) := by
    simp_rw [Fin.prod_univ_succ, Fin.prod_Ioi_zero, Fin.prod_Ioi_succ]
    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)
    rw [h]

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

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

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
v : Fin 0 → R
⊢ (of fun i j => v i ^ ↑j).det = ∏ i : Fin 0, ∏ j ∈ Ioi i, (v j - v i)

Tactic:
exact det_eq_one_of_card_eq_zero (Fintype.card_fin 0)

Result:
no goals

Proof state:
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

Tactic:
rw [det_eq_one_of_card_eq_zero (Fintype.card_fin 0),
det_eq_one_of_card_eq_zero (Fintype.card_fin 0)]

Result:
no goals

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

Tactic:
congr 1

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

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:
simp_rw [of_apply]

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

Proof state:
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

Tactic:
apply det_eq_of_forall_col_eq_smul_add_pred fun _ => v 0

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
⊢ ∀ (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

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

Tactic:
simpa using ih (v ∘ Fin.succ)

Result:
no goals

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

Tactic:
simp

Result:
no goals

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
⊢ (of fun i j => vecCons (v 0 ^ ↑j.succ) (fun i => v i.succ ^ ↑j.succ - v 0 ^ ↑j.succ) (Fin.succAbove 0 i)).det =
    (of fun i j => (v i.succ - v 0) * ∑ k ∈ range (↑j + 1), v i.succ ^ k * v 0 ^ (↑j - k)).det

Tactic:
congr

Result:
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)