awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
a : R
rw :
  Eq.{u_1 + 1} (α := R) (det (n := Fin n) (vandermonde fun (i : Fin n) ↦ v i - a))
    (det (n := Fin n) (vandermonde fun (i : Fin n) ↦ v i + -a))
⊢ det (n := Fin n) (vandermonde fun (i : Fin n) ↦ v i - a) = (vandermonde v).det

Tactic:
rw [← det_vandermonde_add v (-a)]

Premises used: Matrix.det_vandermonde_add, Neg.neg
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
a : R
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin n) (vandermonde fun (i : Fin n) ↦ v i - a))
    (det (n := Fin n) (vandermonde fun (i : Fin n) ↦ v i + -a))

Tactic:
simp only [← sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), Eq.{u_1 + 1} (α := R) (∑ i : Fin n, f j ^ (↑i : ℕ) * v i) 0
⊢ v = 0

Tactic:
eq_zero_of_mulVec_eq_zero (det_vandermonde_ne_zero_iff.mpr hf) (funext hfv)

Premises used: Iff.mpr, Matrix.eq_zero_of_mulVec_eq_zero, funext, Matrix.det_vandermonde_ne_zero_iff
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), Eq.{u_1 + 1} (α := R) (∑ i : Fin n, v i * f j ^ (↑i : ℕ)) 0
apply : ∀ (j : Fin n), Eq.{u_1 + 1} (α := R) (∑ i : Fin n, f j ^ (↑i : ℕ) * v i) 0
⊢ v = 0

Tactic:
apply eq_zero_of_forall_index_sum_pow_mul_eq_zero hf

Premises used: Matrix.eq_zero_of_forall_index_sum_pow_mul_eq_zero
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), Eq.{u_1 + 1} (α := R) (∑ i : Fin n, v i * f j ^ (↑i : ℕ)) 0
simp_rw : ∀ (j : Fin n), Eq.{u_1 + 1} (α := R) (∑ x : Fin n, v x * f j ^ (↑x : ℕ)) 0
⊢ ∀ (j : Fin n), Eq.{u_1 + 1} (α := R) (∑ i : Fin n, f j ^ (↑i : ℕ) * v i) 0

Tactic:
simp_rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), Eq.{u_1 + 1} (α := R) (∑ i : Fin n, v i * f j ^ (↑i : ℕ)) 0
⊢ ∀ (j : Fin n), Eq.{u_1 + 1} (α := R) (∑ x : Fin n, v x * f j ^ (↑x : ℕ)) 0

Tactic:
hfv
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (j : Fin n), Eq.{u_1 + 1} (α := R) (∑ i : Fin n, v i * f j ^ (↑i : ℕ)) 0
⊢ ∀ (j : Fin n), Eq.{u_1 + 1} (α := R) (∑ x : Fin n, v x * f j ^ (↑x : ℕ)) 0

Tactic:
exact hfv
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
f v : Fin n → R
hf : Function.Injective f
hfv : ∀ (i : Fin n), Eq.{u_1 + 1} (α := R) (∑ j : Fin n, v j * f j ^ (↑i : ℕ)) 0
⊢ v = 0

Tactic:
eq_zero_of_vecMul_eq_zero (det_vandermonde_ne_zero_iff.mpr hf) (funext hfv)

Premises used: Iff.mpr, funext, Matrix.det_vandermonde_ne_zero_iff, Matrix.eq_zero_of_vecMul_eq_zero
-- Module: Mathlib.LinearAlgebra.Vandermonde
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 : ℕ)
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
⊢ ((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)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
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 : ℕ))
⊢ (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:
simp_rw [Matrix.mul_apply, eval, Matrix.of_apply, eval₂]

Premises used: Polynomial.eval, Matrix.mul_apply, Polynomial.eval₂, Matrix.of_apply
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
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 : ℕ)))
⊢ 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 only [Matrix.vandermonde]

Premises used: Matrix.vandermonde
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
⊢ (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
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
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 : ℕ)))
⊢ 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:
rw [sum_eq_of_subset _ (fun j => zero_mul ((v i) ^ j)) this, ← Fin.sum_univ_eq_sum_range]

Premises used: Fin.sum_univ_eq_sum_range, Polynomial.sum_eq_of_subset
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
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 : ℕ))
⊢ 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:
congr
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
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 : ℕ))
⊢ 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:
ext k
-- Module: Mathlib.LinearAlgebra.Vandermonde
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 : ℕ)
a₂ a₃ : v i ^ (↑k : ℕ) * (p j).coeff (↑k : ℕ) = 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 : ℕ))

Tactic:
rw [mul_comm, Matrix.of_apply, RingHom.id_apply]

Premises used: RingHom.id_apply, Matrix.of_apply, mul_comm
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
rw₃ rw₄ : (vandermonde v).det = (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) ↦ eval (v i) (p j))

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]

Premises used: Nat.le_of_eq, Matrix.det_mul, Matrix.det_matrixOfPolynomials, mul_one, Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
⊢ 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:
simp
-- Module: Mathlib.LinearAlgebra.Vandermonde
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 :
  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)
⊢ 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:
rw [Nat.superFactorial, det_vandermonde, Fin.prod_univ_succAbove _ 0]

Premises used: Matrix.det_vandermonde, Nat.superFactorial, Fin.prod_univ_succAbove, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Vandermonde
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 :
  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)
⊢ 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:
push_cast
-- Module: Mathlib.LinearAlgebra.Vandermonde
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)
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)
⊢ 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:
congr
-- Module: Mathlib.LinearAlgebra.Vandermonde
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) (∏ x ∈ Ioi 0, (↑(↑x : ℕ) : R)) (↑n.succ.factorial : R)
⊢ Eq.{u_1 + 1} (α := R) (∏ j ∈ Ioi 0, HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑0 : ℕ) : R)) (↑n.succ.factorial : R)

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

Premises used: sub_zero, Nat.cast_zero, Fin.val_zero
-- Module: Mathlib.LinearAlgebra.Vandermonde
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) (↑(∏ i ∈ Ioi 0, (↑i : ℕ)) : R) (↑n.succ.factorial : R)
⊢ Eq.{u_1 + 1} (α := R) (∏ x ∈ Ioi 0, (↑(↑x : ℕ) : R)) (↑n.succ.factorial : R)

Tactic:
norm_cast
-- Module: Mathlib.LinearAlgebra.Vandermonde
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 ∈ Ioi 0, (↑i : ℕ)) : R) (↑n.succ.factorial : R)

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

Premises used: Fin.prod_univ_eq_prod_range, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Vandermonde
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 i, HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑i : ℕ) : R))
    (↑n.superFactorial : R)

Tactic:
rw [det_vandermonde] at hn

Premises used: Matrix.det_vandermonde
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn :
  Eq.{u_1 + 1} (α := R) (∏ i : Fin (n + 1), ∏ j ∈ Ioi i, HSub.hSub (α := R) (↑(↑j : ℕ) : R) (↑(↑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)

Tactic:
simp [hn]
-- Module: Mathlib.LinearAlgebra.Vandermonde
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)
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)
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(↑i : ℕ) : R)))
    (↑n.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]

Premises used: Matrix.det_vandermonde, Nat.superFactorial, Fin.succ, sub_zero, Fin.prod_univ_succAbove, Fin.prod_univ_eq_prod_range, HAdd.hAdd, Nat.cast_zero, OfNat.ofNat, Matrix.zero, Fin.val_zero
-- Module: Mathlib.LinearAlgebra.Vandermonde
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) ↦
        HMul.hMul (α := ℤ) (β := ℤ) ((↑(↑j : ℕ).factorial : ℤ) : ℤ)
          ((of : (a : Fin n → Fin n → ℤ) → Matrix (Fin n) (Fin n) ℤ)
              (fun (i j : Fin n) ↦ (↑((v i).choose (↑j : ℕ)) : ℤ)) i 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 : ℕ)) : ℤ)))

Tactic:
det_mul_row (fun (i : Fin n) => ((Nat.factorial (i : ℕ)) : ℤ)) _

Premises used: Fin.val, Nat.cast, Nat.factorial, Matrix.det_mul_row
-- Module: Mathlib.LinearAlgebra.Vandermonde
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 :
          ℤ)
h₁ : Eq (α := ℤ) (↑(∏ i : Fin n, (↑i : ℕ).factorial) : ℤ) (∏ 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) ↦
        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 : ℕ)) : ℤ)))

Tactic:
convert! det_mul_row (fun (i : Fin n) => ((Nat.factorial (i : ℕ)) : ℤ)) _

Premises used: Fin.val, Nat.cast, Nat.factorial, Matrix.det_mul_row
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
n : ℕ
v : Fin n → ℕ
x x_1 : Fin n
h :
  (↑((v x).descFactorial (↑x_1 : ℕ)) : ℤ) =
    HMul.hMul (α := ℤ) (↑(↑x_1 : ℕ).factorial : ℤ) (↑((v x).choose (↑x_1 : ℕ)) : ℤ)
⊢ 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:
rw [of_apply, descPochhammer_eval_eq_descFactorial ℤ _ _]

Premises used: Int, Matrix.of_apply, descPochhammer_eval_eq_descFactorial
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
n : ℕ
v : Fin n → ℕ
x x_1 : Fin n
h : (v x).descFactorial (↑x_1 : ℕ) = (↑x_1 : ℕ).factorial * (v x).choose (↑x_1 : ℕ)
⊢ (↑((v x).descFactorial (↑x_1 : ℕ)) : ℤ) =
    HMul.hMul (α := ℤ) (↑(↑x_1 : ℕ).factorial : ℤ) (↑((v x).choose (↑x_1 : ℕ)) : ℤ)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
n : ℕ
v : Fin n → ℕ
x x_1 : Fin n
⊢ (v x).descFactorial (↑x_1 : ℕ) = (↑x_1 : ℕ).factorial * (v x).choose (↑x_1 : ℕ)

Tactic:
Nat.descFactorial_eq_factorial_mul_choose _ _

Premises used: Nat.descFactorial_eq_factorial_mul_choose
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
n : ℕ
v : Fin n → ℕ
x x_1 : Fin n
⊢ (v x).descFactorial (↑x_1 : ℕ) = (↑x_1 : ℕ).factorial * (v x).choose (↑x_1 : ℕ)

Tactic:
exact Nat.descFactorial_eq_factorial_mul_choose _ _

Premises used: Nat.descFactorial_eq_factorial_mul_choose
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
n : ℕ
v : Fin n → ℕ
h h₁ : Eq (α := ℤ) (∏ i : Fin n, (↑(↑i : ℕ).factorial : ℤ)) (∏ i : Fin n, (↑(↑i : ℕ).factorial : ℤ))
⊢ Eq (α := ℤ) (↑(∏ i : Fin n, (↑i : ℕ).factorial) : ℤ) (∏ i : Fin n, (↑(↑i : ℕ).factorial : ℤ))

Tactic:
rw [Nat.cast_prod]

Premises used: Nat.cast_prod
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := inf' univ ⋯ v
w' : (i : Fin (n + 1)) → ℕ := fun (i : Fin (n + 1)) ↦ (v i - m).toNat
⊢ ∀ (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 _))
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
⊢ 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)
-- Module: Mathlib.LinearAlgebra.Vandermonde
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)))
simp : (vandermonde v).det
| det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(w' i) : ℤ))

Tactic:
simp only [hw', det_vandermonde_sub]

Premises used: Matrix.det_vandermonde_sub
-- Module: Mathlib.LinearAlgebra.Vandermonde
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)))
⊢ (vandermonde v).det =
    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:
conv_lhs at h => simp only [hw', det_vandermonde_sub]

Premises used: Matrix.det_vandermonde_sub