-- Mathlib/Data/Nat/Factorial/SuperFactorial.lean
theorem superFactorial_dvd_vandermonde_det {n : ℕ} (v : Fin (n + 1) → ℤ) :
    ↑(Nat.superFactorial n) ∣ (Matrix.vandermonde v).det

Proof state:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
⊢ ↑(sf n) ∣ (Matrix.vandermonde v).det

Tactic:
let w' := fun i ↦ (v i - m).toNat

Result:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat
⊢ ↑(sf n) ∣ (Matrix.vandermonde v).det

Proof state:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat
⊢ ↑(sf n) ∣ (Matrix.vandermonde v).det

Tactic:
have hw' : ∀ i, (w' i : ℤ) = v i - m := fun i ↦ Int.toNat_sub_of_le (inf'_le _ (mem_univ _))

Result:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m
⊢ ↑(sf n) ∣ (Matrix.vandermonde v).det

Proof state:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m
h :
  (Matrix.vandermonde fun i => ↑(w' i)).det =
    (Matrix.of fun i j => Polynomial.eval ((fun i => ↑(w' i)) i) ((fun i => descPochhammer ℤ ↑i) j)).det
⊢ ↑(sf n) ∣ (Matrix.vandermonde v).det

Tactic:
conv_lhs at h => simp only [hw', Matrix.det_vandermonde_sub]

Result:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m
h :
  (Matrix.vandermonde v).det =
    (Matrix.of fun i j => Polynomial.eval ((fun i => ↑(w' i)) i) ((fun i => descPochhammer ℤ ↑i) j)).det
⊢ ↑(sf n) ∣ (Matrix.vandermonde v).det

Proof state:
n : ℕ
v : Fin (n + 1) → ℤ
⊢ ↑(sf n) ∣ (Matrix.vandermonde v).det

Tactic:
let m := inf' univ ⟨0, mem_univ _⟩ v

Result:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
⊢ ↑(sf n) ∣ (Matrix.vandermonde v).det

Proof state:
case h
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m
h :
  (Matrix.vandermonde v).det =
    (Matrix.of fun i j => Polynomial.eval ((fun i => ↑(w' i)) i) ((fun i => descPochhammer ℤ ↑i) j)).det
⊢ (Matrix.vandermonde v).det = ↑(sf n) * (Matrix.of fun i j => ↑((w' i).choose ↑j)).det

Tactic:
simp [h, matrixOf_eval_descPochhammer_eq_mul_matrixOf_choose w', Fin.prod_univ_eq_prod_range]

Result:
no goals

Proof state:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m
h :
  (Matrix.vandermonde v).det =
    (Matrix.of fun i j => Polynomial.eval ((fun i => ↑(w' i)) i) ((fun i => descPochhammer ℤ ↑i) j)).det
⊢ ↑(sf n) ∣ (Matrix.vandermonde v).det

Tactic:
use (Matrix.of (fun (i j : Fin (n + 1)) => (Nat.choose (w' i) (j : ℕ) : ℤ))).det

Result:
case h
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m
h :
  (Matrix.vandermonde v).det =
    (Matrix.of fun i j => Polynomial.eval ((fun i => ↑(w' i)) i) ((fun i => descPochhammer ℤ ↑i) j)).det
⊢ (Matrix.vandermonde v).det = ↑(sf n) * (Matrix.of fun i j => ↑((w' i).choose ↑j)).det

Proof state:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m
⊢ ↑(sf n) ∣ (Matrix.vandermonde v).det

Tactic:
have h := Matrix.det_eval_matrixOfPolynomials_eq_det_vandermonde (fun i ↦ ↑(w' i))
    (fun i => descPochhammer ℤ i)
    (fun i => descPochhammer_natDegree ℤ i)
    (fun i => monic_descPochhammer ℤ i)

Result:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := univ.inf' ⋯ v
w' : Fin (n + 1) → ℕ := fun i => (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), ↑(w' i) = v i - m
h :
  (Matrix.vandermonde fun i => ↑(w' i)).det =
    (Matrix.of fun i j => Polynomial.eval ((fun i => ↑(w' i)) i) ((fun i => descPochhammer ℤ ↑i) j)).det
⊢ ↑(sf n) ∣ (Matrix.vandermonde v).det