awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ (↑i : ℕ)
⊢ ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ eval (v i) (p j)) =
    HMul.hMul (β := Matrix (Fin n) (Fin n) R) (vandermonde v)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ) :
        Matrix (Fin n) (Fin n) R)
have a : ∀ (i j : Fin n),
  (of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ eval (v i) (p j)) i j =
    HMul.hMul (β := Matrix (Fin n) (Fin n) R) (vandermonde v)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ) :
        Matrix (Fin n) (Fin n) R)
      i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ (↑i : ℕ)
i j : Fin n
⊢ (of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ eval (v i) (p j)) i j =
    HMul.hMul (β := Matrix (Fin n) (Fin n) R) (vandermonde v)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ) :
        Matrix (Fin n) (Fin n) R)
      i j
have a : Eq (α := R) ((p j).sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (v i ^ e))
  (∑ x : Fin n, vandermonde v i x * (p j).coeff (↑x : ℕ))
Tactic: simp_rw [Matrix.mul_apply, eval, Matrix.of_apply, eval₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ (↑i : ℕ)
i j : Fin n
⊢ Eq (α := R) ((p j).sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (v i ^ e))
    (∑ x : Fin n, vandermonde v i x * (p j).coeff (↑x : ℕ))
have a : Eq (α := R) ((p j).sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (v i ^ e))
  (∑ x : Fin n,
    HMul.hMul (α := R)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ v i ^ (↑j : ℕ)) i x : R)
      ((p j).coeff (↑x : ℕ)))
Tactic: simp only [Matrix.vandermonde]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ (↑i : ℕ)
i j : Fin n
⊢ Eq (α := R) ((p j).sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (v i ^ e))
    (∑ x : Fin n,
      HMul.hMul (α := R)
        ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ v i ^ (↑j : ℕ)) i x : R)
        ((p j).coeff (↑x : ℕ)))
have this : (p j).support ⊆ range n
Tactic: have : (p j).support ⊆ range n := supp_subset_range <| Nat.lt_of_le_of_lt (h_deg j) <| Fin.prop j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ (↑i : ℕ)
i j : Fin n
this : (p j).support ⊆ range n
⊢ Eq (α := R) ((p j).sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (v i ^ e))
    (∑ x : Fin n,
      HMul.hMul (α := R)
        ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ v i ^ (↑j : ℕ)) i x : R)
        ((p j).coeff (↑x : ℕ)))
have a : Eq.{u_1 + 1} (α := R)
  (∑ i_1 : Fin n, HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) ((p j).coeff (↑i_1 : ℕ)) : R) (v i ^ (↑i_1 : ℕ)))
  (∑ x : Fin n,
    HMul.hMul (α := R)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ v i ^ (↑j : ℕ)) i x : R)
      ((p j).coeff (↑x : ℕ)))
Tactic: rw [sum_eq_of_subset _ (fun j => zero_mul ((v i) ^ j)) this, ← Fin.sum_univ_eq_sum_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ (↑i : ℕ)
i j : Fin n
this : (p j).support ⊆ range n
⊢ Eq.{u_1 + 1} (α := R)
    (∑ i_1 : Fin n, HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) ((p j).coeff (↑i_1 : ℕ)) : R) (v i ^ (↑i_1 : ℕ)))
    (∑ x : Fin n,
      HMul.hMul (α := R)
        ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ v i ^ (↑j : ℕ)) i x : R)
        ((p j).coeff (↑x : ℕ)))
have a : Eq.{u_1 + 1} (α := Fin n → R)
  (fun (i_1 : Fin n) ↦
    HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) ((p j).coeff (↑i_1 : ℕ)) : R) (v i ^ (↑i_1 : ℕ)))
  fun (x : Fin n) ↦
  HMul.hMul (α := R)
    ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ v i ^ (↑j : ℕ)) i x : R)
    ((p j).coeff (↑x : ℕ))
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ (↑i : ℕ)
i j : Fin n
this : (p j).support ⊆ range n
⊢ Eq.{u_1 + 1} (α := Fin n → R)
    (fun (i_1 : Fin n) ↦
      HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) ((p j).coeff (↑i_1 : ℕ)) : R) (v i ^ (↑i_1 : ℕ)))
    fun (x : Fin n) ↦
    HMul.hMul (α := R)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ v i ^ (↑j : ℕ)) i x : R)
      ((p j).coeff (↑x : ℕ))
have a : ∀ (k : Fin n),
  HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) ((p j).coeff (↑k : ℕ)) : R) (v i ^ (↑k : ℕ)) =
    HMul.hMul (α := R)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ v i ^ (↑j : ℕ)) i k : R)
      ((p j).coeff (↑k : ℕ))
Tactic: ext k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ (↑i : ℕ)
i j : Fin n
this : (p j).support ⊆ range n
k : Fin n
⊢ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) ((p j).coeff (↑k : ℕ)) : R) (v i ^ (↑k : ℕ)) =
    HMul.hMul (α := R)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ v i ^ (↑j : ℕ)) i k : R)
      ((p j).coeff (↑k : ℕ))
have a : HMul.hMul (β := R) (v i ^ (↑k : ℕ)) ((RingHom.id R : (a : R) → R) ((p j).coeff (↑k : ℕ)) : R) =
  HMul.hMul (α := R)
    ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ v i ^ (↑j : ℕ)) i k : R)
    ((p j).coeff (↑k : ℕ))
Tactic: rw [mul_comm, Matrix.of_apply, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ (↑i : ℕ)
i j : Fin n
this : (p j).support ⊆ range n
k : Fin n
a :
  HMul.hMul (β := R) (v i ^ (↑k : ℕ)) ((RingHom.id R : (a : R) → R) ((p j).coeff (↑k : ℕ)) : R) =
    HMul.hMul (α := R)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ v i ^ (↑j : ℕ)) i k : R)
      ((p j).coeff (↑k : ℕ))
⊢ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) ((p j).coeff (↑k : ℕ)) : R) (v i ^ (↑k : ℕ)) =
    HMul.hMul (α := R)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ v i ^ (↑j : ℕ)) i k : R)
      ((p j).coeff (↑k : ℕ))
have a₁ : HMul.hMul (β := R) (v i ^ (↑k : ℕ)) ((RingHom.id R : (a : R) → R) ((p j).coeff (↑k : ℕ)) : R) =
  v i ^ (↑k : ℕ) * (p j).coeff (↑k : ℕ)
Tactic: rw [mul_comm, Matrix.of_apply, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ (↑i : ℕ)
i j : Fin n
this : (p j).support ⊆ range n
k : Fin n
a :
  HMul.hMul (β := R) (v i ^ (↑k : ℕ)) ((RingHom.id R : (a : R) → R) ((p j).coeff (↑k : ℕ)) : R) =
    HMul.hMul (α := R)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ v i ^ (↑j : ℕ)) i k : R)
      ((p j).coeff (↑k : ℕ))
a₁ :
  HMul.hMul (β := R) (v i ^ (↑k : ℕ)) ((RingHom.id R : (a : R) → R) ((p j).coeff (↑k : ℕ)) : R) =
    v i ^ (↑k : ℕ) * (p j).coeff (↑k : ℕ)
⊢ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) ((p j).coeff (↑k : ℕ)) : R) (v i ^ (↑k : ℕ)) =
    HMul.hMul (α := R)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) (fun (i j : Fin n) ↦ v i ^ (↑j : ℕ)) i k : R)
      ((p j).coeff (↑k : ℕ))
have a₂ : v i ^ (↑k : ℕ) * (p j).coeff (↑k : ℕ) = v i ^ (↑k : ℕ) * (p j).coeff (↑k : ℕ)
Tactic: rw [mul_comm, Matrix.of_apply, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = (↑i : ℕ)
h_monic : ∀ (i : Fin n), (p i).Monic
⊢ (vandermonde v).det =
    det (n := Fin n) ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ eval (v i) (p j))
have rw : (vandermonde v).det =
  (HMul.hMul (β := Matrix (Fin n) (Fin n) R) (vandermonde v)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ) :
        Matrix (Fin n) (Fin n) R)).det
Tactic: rw [Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials v p (fun i ↦
      Nat.le_of_eq (h_deg i)), Matrix.det_mul,
      Matrix.det_matrixOfPolynomials p h_deg h_monic, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = (↑i : ℕ)
h_monic : ∀ (i : Fin n), (p i).Monic
rw :
  (vandermonde v).det =
    (HMul.hMul (β := Matrix (Fin n) (Fin n) R) (vandermonde v)
        ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ) :
          Matrix (Fin n) (Fin n) R)).det
⊢ (vandermonde v).det =
    det (n := Fin n) ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ eval (v i) (p j))
have rw₁ : (vandermonde v).det =
  (vandermonde v).det *
    det (n := Fin n)
      ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ))
Tactic: rw [Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials v p (fun i ↦
      Nat.le_of_eq (h_deg i)), Matrix.det_mul,
      Matrix.det_matrixOfPolynomials p h_deg h_monic, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = (↑i : ℕ)
h_monic : ∀ (i : Fin n), (p i).Monic
rw :
  (vandermonde v).det =
    (HMul.hMul (β := Matrix (Fin n) (Fin n) R) (vandermonde v)
        ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ) :
          Matrix (Fin n) (Fin n) R)).det
rw₁ :
  (vandermonde v).det =
    (vandermonde v).det *
      det (n := Fin n)
        ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ))
⊢ (vandermonde v).det =
    det (n := Fin n) ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ eval (v i) (p j))
have rw₂ : (vandermonde v).det = (vandermonde v).det * 1
Tactic: rw [Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials v p (fun i ↦
      Nat.le_of_eq (h_deg i)), Matrix.det_mul,
      Matrix.det_matrixOfPolynomials p h_deg h_monic, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = (↑i : ℕ)
h_monic : ∀ (i : Fin n), (p i).Monic
rw :
  (vandermonde v).det =
    (HMul.hMul (β := Matrix (Fin n) (Fin n) R) (vandermonde v)
        ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ) :
          Matrix (Fin n) (Fin n) R)).det
rw₁ :
  (vandermonde v).det =
    (vandermonde v).det *
      det (n := Fin n)
        ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ (p j).coeff (↑i : ℕ))
rw₂ : (vandermonde v).det = (vandermonde v).det * 1
⊢ (vandermonde v).det =
    det (n := Fin n) ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ eval (v i) (p j))
have rw₃ : (vandermonde v).det = (vandermonde v).det
Tactic: rw [Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials v p (fun i ↦
      Nat.le_of_eq (h_deg i)), Matrix.det_mul,
      Matrix.det_matrixOfPolynomials p h_deg h_monic, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn :
  Eq.{u_1 + 1} (α := R) (det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(↑i : ℕ) : R)))
    (↑n.superFactorial : R)
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin (n + 1 + 1)) (vandermonde fun (i : Fin (n + 1 + 1)) ↦ (↑(↑i : ℕ) : R)))
    (↑(n + 1).superFactorial : R)
have succ : HMul.hMul (α := R) (∏ j ∈ Ioi 0, HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑0 : ℕ) : R))
    (∏ i : Fin (n + 1), ∏ j ∈ Ioi (succAbove 0 i), HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑(succAbove 0 i) : ℕ) : R)) =
  (↑(n.succ.factorial * n.superFactorial) : R)
Tactic: rw [Nat.superFactorial, det_vandermonde, Fin.prod_univ_succAbove _ 0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn :
  Eq.{u_1 + 1} (α := R) (det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(↑i : ℕ) : R)))
    (↑n.superFactorial : R)
⊢ HMul.hMul (α := R) (∏ j ∈ Ioi 0, HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑0 : ℕ) : R))
      (∏ i : Fin (n + 1), ∏ j ∈ Ioi (succAbove 0 i), HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑(succAbove 0 i) : ℕ) : R)) =
    (↑(n.succ.factorial * n.superFactorial) : R)
have succ : HMul.hMul (α := R) (∏ j ∈ Ioi 0, HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑0 : ℕ) : R))
    (∏ i : Fin (n + 1), ∏ j ∈ Ioi (succAbove 0 i), HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑(succAbove 0 i) : ℕ) : R)) =
  HMul.hMul (α := R) (↑n.succ.factorial : R) (↑n.superFactorial : R)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn :
  Eq.{u_1 + 1} (α := R) (det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(↑i : ℕ) : R)))
    (↑n.superFactorial : R)
⊢ HMul.hMul (α := R) (∏ j ∈ Ioi 0, HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑0 : ℕ) : R))
      (∏ i : Fin (n + 1), ∏ j ∈ Ioi (succAbove 0 i), HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑(succAbove 0 i) : ℕ) : R)) =
    HMul.hMul (α := R) (↑n.succ.factorial : R) (↑n.superFactorial : R)
have succ : Eq.{u_1 + 1} (α := R) (∏ j ∈ Ioi 0, HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑0 : ℕ) : R)) (↑n.succ.factorial : R)
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn :
  Eq.{u_1 + 1} (α := R) (det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(↑i : ℕ) : R)))
    (↑n.superFactorial : R)
succ : Eq.{u_1 + 1} (α := R) (∏ j ∈ Ioi 0, HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑0 : ℕ) : R)) (↑n.succ.factorial : R)
⊢ HMul.hMul (α := R) (∏ j ∈ Ioi 0, HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑0 : ℕ) : R))
      (∏ i : Fin (n + 1), ∏ j ∈ Ioi (succAbove 0 i), HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑(succAbove 0 i) : ℕ) : R)) =
    HMul.hMul (α := R) (↑n.succ.factorial : R) (↑n.superFactorial : R)
have succ₁ : Eq.{u_1 + 1} (α := R)
  (∏ i : Fin (n + 1), ∏ j ∈ Ioi (succAbove 0 i), HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑(succAbove 0 i) : ℕ) : R))
  (↑n.superFactorial : R)
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn :
  Eq.{u_1 + 1} (α := R) (det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(↑i : ℕ) : R)))
    (↑n.superFactorial : R)
⊢ Eq.{u_1 + 1} (α := R) (∏ j ∈ Ioi 0, HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑0 : ℕ) : R)) (↑n.succ.factorial : R)
have succ : Eq.{u_1 + 1} (α := R) (∏ x ∈ Ioi 0, (↑(↑x : ℕ) : R)) (↑n.succ.factorial : R)
Tactic: simp only [Fin.val_zero, Nat.cast_zero, sub_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn :
  Eq.{u_1 + 1} (α := R) (det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(↑i : ℕ) : R)))
    (↑n.superFactorial : R)
⊢ Eq.{u_1 + 1} (α := R) (∏ x ∈ Ioi 0, (↑(↑x : ℕ) : R)) (↑n.succ.factorial : R)
have succ : Eq.{u_1 + 1} (α := R) (↑(∏ i ∈ Ioi 0, (↑i : ℕ)) : R) (↑n.succ.factorial : R)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn :
  Eq.{u_1 + 1} (α := R) (det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(↑i : ℕ) : R)))
    (↑n.superFactorial : R)
⊢ Eq.{u_1 + 1} (α := R)
    (∏ i : Fin (n + 1), ∏ j ∈ Ioi (succAbove 0 i), HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑(succAbove 0 i) : ℕ) : R))
    (↑n.superFactorial : R)
have hn₁ : Eq.{u_1 + 1} (α := R) (∏ i : Fin (n + 1), ∏ j ∈ Ioi i, HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑i : ℕ) : R))
  (↑n.superFactorial : R)
Tactic: rw [det_vandermonde] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(↑i : ℕ) : R)))
    (↑n.superFactorial : R)
have zero : Eq.{u_1 + 1} (α := R)
  (det (n := Fin (HAdd.hAdd (α := ℕ) 0 1)) (vandermonde fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ (↑(↑i : ℕ) : R)))
  (↑(Nat.superFactorial 0) : R)
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [Nat.superFactorial, det_vandermonde, Fin.prod_univ_succAbove _ 0]
    push_cast
    congr
    · simp only [Fin.val_zero, Nat.cast_zero, sub_zero]
      norm_cast
      simp [Fin.prod_univ_eq_prod_range (fun i ↦ (↑i + 1)) (n + 1)]
    · rw [det_vandermonde] at hn
      simp [hn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
zero :
  Eq.{u_1 + 1} (α := R)
    (det (n := Fin (HAdd.hAdd (α := ℕ) 0 1)) (vandermonde fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ (↑(↑i : ℕ) : R)))
    (↑(Nat.superFactorial 0) : R)
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(↑i : ℕ) : R)))
    (↑n.superFactorial : R)
have succ : ∀ (n : ℕ)
  (hn :
    Eq.{u_1 + 1} (α := R) (det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(↑i : ℕ) : R)))
      (↑n.superFactorial : R)),
  Eq.{u_1 + 1} (α := R) (det (n := Fin (n + 1 + 1)) (vandermonde fun (i : Fin (n + 1 + 1)) ↦ (↑(↑i : ℕ) : R)))
    (↑(n + 1).superFactorial : R)
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [Nat.superFactorial, det_vandermonde, Fin.prod_univ_succAbove _ 0]
    push_cast
    congr
    · simp only [Fin.val_zero, Nat.cast_zero, sub_zero]
      norm_cast
      simp [Fin.prod_univ_eq_prod_range (fun i ↦ (↑i + 1)) (n + 1)]
    · rw [det_vandermonde] at hn
      simp [hn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
n : ℕ
v : Fin n → ℕ
⊢ det (n := Fin n)
      ((of : (a : Fin n → Fin n → ℤ) → Matrix (Fin n) (Fin n) ℤ) fun (i j : Fin n) ↦
        eval (↑(v i) : ℤ) (descPochhammer ℤ (↑j : ℕ))) =
    HMul.hMul (α := ℤ) (↑(∏ i : Fin n, (↑i : ℕ).factorial) : ℤ)
      (det (n := Fin n)
        ((of : (a : Fin n → Fin n → ℤ) → Matrix (Fin n) (Fin n) ℤ) fun (i j : Fin n) ↦ (↑((v i).choose (↑j : ℕ)) : ℤ)))
have h : ∀ (x x_1 : Fin n),
  eval (↑(v x) : ℤ) (descPochhammer ℤ (↑x_1 : ℕ)) =
    HMul.hMul (α := ℤ) (β := ℤ) ((↑(↑x_1 : ℕ).factorial : ℤ) : ℤ)
      ((of : (a : Fin n → Fin n → ℤ) → Matrix (Fin n) (Fin n) ℤ) (fun (i j : Fin n) ↦ (↑((v i).choose (↑j : ℕ)) : ℤ)) x
          x_1 :
        ℤ)
Tactic: convert! det_mul_row (fun (i : Fin n) => ((Nat.factorial (i : ℕ)) : ℤ)) _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
n : ℕ
v : Fin n → ℕ
h :
  ∀ (x x_1 : Fin n),
    eval (↑(v x) : ℤ) (descPochhammer ℤ (↑x_1 : ℕ)) =
      HMul.hMul (α := ℤ) (β := ℤ) ((↑(↑x_1 : ℕ).factorial : ℤ) : ℤ)
        ((of : (a : Fin n → Fin n → ℤ) → Matrix (Fin n) (Fin n) ℤ) (fun (i j : Fin n) ↦ (↑((v i).choose (↑j : ℕ)) : ℤ))
            x x_1 :
          ℤ)
⊢ det (n := Fin n)
      ((of : (a : Fin n → Fin n → ℤ) → Matrix (Fin n) (Fin n) ℤ) fun (i j : Fin n) ↦
        eval (↑(v i) : ℤ) (descPochhammer ℤ (↑j : ℕ))) =
    HMul.hMul (α := ℤ) (↑(∏ i : Fin n, (↑i : ℕ).factorial) : ℤ)
      (det (n := Fin n)
        ((of : (a : Fin n → Fin n → ℤ) → Matrix (Fin n) (Fin n) ℤ) fun (i j : Fin n) ↦ (↑((v i).choose (↑j : ℕ)) : ℤ)))
have h₁ : Eq (α := ℤ) (↑(∏ i : Fin n, (↑i : ℕ).factorial) : ℤ) (∏ i : Fin n, (↑(↑i : ℕ).factorial : ℤ))
Tactic: convert! det_mul_row (fun (i : Fin n) => ((Nat.factorial (i : ℕ)) : ℤ)) _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
n : ℕ
v : Fin n → ℕ
x x_1 : Fin n
⊢ eval (↑(v x) : ℤ) (descPochhammer ℤ (↑x_1 : ℕ)) =
    HMul.hMul (α := ℤ) (β := ℤ) ((↑(↑x_1 : ℕ).factorial : ℤ) : ℤ)
      ((of : (a : Fin n → Fin n → ℤ) → Matrix (Fin n) (Fin n) ℤ) (fun (i j : Fin n) ↦ (↑((v i).choose (↑j : ℕ)) : ℤ)) x
          x_1 :
        ℤ)
have h : (↑((v x).descFactorial (↑x_1 : ℕ)) : ℤ) =
  HMul.hMul (α := ℤ) (↑(↑x_1 : ℕ).factorial : ℤ) (↑((v x).choose (↑x_1 : ℕ)) : ℤ)
Tactic: rw [of_apply, descPochhammer_eval_eq_descFactorial ℤ _ _]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
n : ℕ
v : Fin n → ℕ
x x_1 : Fin n
⊢ (↑((v x).descFactorial (↑x_1 : ℕ)) : ℤ) =
    HMul.hMul (α := ℤ) (↑(↑x_1 : ℕ).factorial : ℤ) (↑((v x).choose (↑x_1 : ℕ)) : ℤ)
have h : (v x).descFactorial (↑x_1 : ℕ) = (↑x_1 : ℕ).factorial * (v x).choose (↑x_1 : ℕ)
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
n : ℕ
v : Fin n → ℕ
⊢ Eq (α := ℤ) (↑(∏ i : Fin n, (↑i : ℕ).factorial) : ℤ) (∏ i : Fin n, (↑(↑i : ℕ).factorial : ℤ))
have h : Eq (α := ℤ) (∏ i : Fin n, (↑(↑i : ℕ).factorial : ℤ)) (∏ i : Fin n, (↑(↑i : ℕ).factorial : ℤ))
Tactic: rw [Nat.cast_prod]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (hypothesis)
Goal:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := inf' univ ⋯ v
w' : (i : Fin (n + 1)) → ℕ := fun (i : Fin (n + 1)) ↦ (v i - m).toNat
⊢ (↑n.superFactorial : ℤ) ∣ (vandermonde v).det
have hw' : ∀ (i : Fin (n + 1)), (↑(w' i) : ℤ) = v i - m
Tactic: have hw' : ∀ i, (w' i : ℤ) = v i - m := fun i ↦ Int.toNat_sub_of_le (inf'_le _ (mem_univ _))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (hypothesis)
Goal:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := inf' univ ⋯ v
w' : (i : Fin (n + 1)) → ℕ := fun (i : Fin (n + 1)) ↦ (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), (↑(w' i) : ℤ) = v i - m
⊢ (↑n.superFactorial : ℤ) ∣ (vandermonde v).det
have h : Eq (α := ℤ) (det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(w' i) : ℤ)))
  (det (n := Fin (n + 1))
    ((of : (a : Fin (n + 1) → Fin (n + 1) → ℤ) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ) fun (i j : Fin (n + 1)) ↦
      eval ((fun (i : Fin (n + 1)) ↦ ((↑(w' i) : ℤ) : ℤ)) i)
        ((fun (i : Fin (n + 1)) ↦ (descPochhammer ℤ (↑i : ℕ) : ℤ[X])) j)))
Tactic: have h := det_eval_matrixOfPolynomials_eq_det_vandermonde (fun i ↦ ↑(w' i))
      (fun i => descPochhammer ℤ i)
      (fun i => descPochhammer_natDegree ℤ i)
      (fun i => monic_descPochhammer ℤ i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := inf' univ ⋯ v
w' : (i : Fin (n + 1)) → ℕ := fun (i : Fin (n + 1)) ↦ (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), (↑(w' i) : ℤ) = v i - m
h :
  Eq (α := ℤ) (det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(w' i) : ℤ)))
    (det (n := Fin (n + 1))
      ((of : (a : Fin (n + 1) → Fin (n + 1) → ℤ) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ) fun (i j : Fin (n + 1)) ↦
        eval ((fun (i : Fin (n + 1)) ↦ ((↑(w' i) : ℤ) : ℤ)) i)
          ((fun (i : Fin (n + 1)) ↦ (descPochhammer ℤ (↑i : ℕ) : ℤ[X])) j)))
| det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(w' i) : ℤ))
have simp : (vandermonde v).det
Tactic: simp only [hw', det_vandermonde_sub]