-- Mathlib/Data/Nat/Factorial/SuperFactorial.lean
theorem det_vandermonde_id_eq_superFactorial (n : ℕ) :
    (Matrix.vandermonde (fun (i : Fin (n + 1)) ↦ (i : R))).det = Nat.superFactorial n

Proof state:
case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)
⊢ ↑(∏ x ∈ Ioi 0, ↑x) = ↑n.succ !

Tactic:
simp [Fin.prod_univ_eq_prod_range (fun i ↦ (↑i + 1)) (n + 1)]

Result:
no goals

Proof state:
case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (↑↑j - ↑↑i) = ↑(sf n)
⊢ ∏ i : Fin (n + 1), ∏ j ∈ Ioi (Fin.succAbove 0 i), (↑↑j - ↑↑(Fin.succAbove 0 i)) = ↑(sf n)

Tactic:
simp [hn]

Result:
no goals

Proof state:
case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)
⊢ ∏ x ∈ Ioi 0, ↑↑x = ↑n.succ !

Tactic:
norm_cast

Result:
case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)
⊢ ↑(∏ x ∈ Ioi 0, ↑x) = ↑n.succ !

Proof state:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)
⊢ (∏ j ∈ Ioi 0, (↑↑j - ↑↑0)) * ∏ i : Fin (n + 1), ∏ j ∈ Ioi (Fin.succAbove 0 i), (↑↑j - ↑↑(Fin.succAbove 0 i)) =
    ↑n.succ ! * ↑(sf n)

Tactic:
congr

Result:
case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)
⊢ ∏ j ∈ Ioi 0, (↑↑j - ↑↑0) = ↑n.succ !

case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)
⊢ ∏ i : Fin (n + 1), ∏ j ∈ Ioi (Fin.succAbove 0 i), (↑↑j - ↑↑(Fin.succAbove 0 i)) = ↑(sf n)

Proof state:
case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)
⊢ ∏ j ∈ Ioi 0, (↑↑j - ↑↑0) = ↑n.succ !

Tactic:
simp only [Fin.val_zero, Nat.cast_zero, sub_zero]

Result:
case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)
⊢ ∏ x ∈ Ioi 0, ↑↑x = ↑n.succ !

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
⊢ (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf 0)

Tactic:
simp [Matrix.det_vandermonde]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)
⊢ (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n + 1)

Tactic:
rw [Nat.superFactorial, Matrix.det_vandermonde, Fin.prod_univ_succAbove _ 0]

Result:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)
⊢ (∏ j ∈ Ioi 0, (↑↑j - ↑↑0)) * ∏ i : Fin (n + 1), ∏ j ∈ Ioi (Fin.succAbove 0 i), (↑↑j - ↑↑(Fin.succAbove 0 i)) =
    ↑(n.succ ! * sf n)

Proof state:
case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)
⊢ ∏ i : Fin (n + 1), ∏ j ∈ Ioi (Fin.succAbove 0 i), (↑↑j - ↑↑(Fin.succAbove 0 i)) = ↑(sf n)

Tactic:
rw [Matrix.det_vandermonde] at hn

Result:
case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (↑↑j - ↑↑i) = ↑(sf n)
⊢ ∏ i : Fin (n + 1), ∏ j ∈ Ioi (Fin.succAbove 0 i), (↑↑j - ↑↑(Fin.succAbove 0 i)) = ↑(sf n)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)

Tactic:
induction' n with n hn

Result:
case zero
R : Type u_1
inst✝ : CommRing R
⊢ (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf 0)

case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)
⊢ (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n + 1)

Proof state:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)
⊢ (∏ j ∈ Ioi 0, (↑↑j - ↑↑0)) * ∏ i : Fin (n + 1), ∏ j ∈ Ioi (Fin.succAbove 0 i), (↑↑j - ↑↑(Fin.succAbove 0 i)) =
    ↑(n.succ ! * sf n)

Tactic:
push_cast

Result:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (Matrix.vandermonde fun i => ↑↑i).det = ↑(sf n)
⊢ (∏ j ∈ Ioi 0, (↑↑j - ↑↑0)) * ∏ i : Fin (n + 1), ∏ j ∈ Ioi (Fin.succAbove 0 i), (↑↑j - ↑↑(Fin.succAbove 0 i)) =
    ↑n.succ ! * ↑(sf n)