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 : ℕ
R' : Type u_3
inst_1 : CommRing R'
φ : R →+* R'
v w : Fin n → R
⊢ Eq.{u_3 + 1} (α := Matrix (Fin n) (Fin n) R')
    (projVandermonde (fun (i : Fin n) ↦ (φ : (a : R) → R') (v i)) fun (i : Fin n) ↦ (φ : (a : R) → R') (w i))
    (((φ.mapMatrix : RingHom.{u_1, u_3} (Matrix (Fin n) (Fin n) R) (Matrix (Fin n) (Fin n) R')) :
        (a : Matrix (Fin n) (Fin n) R) → Matrix (Fin n) (Fin n) R')
      (projVandermonde v w))
have a : ∀ (i j : Fin n),
  Eq.{u_3 + 1} (α := R')
    (projVandermonde (fun (i : Fin n) ↦ (φ : (a : R) → R') (v i)) (fun (i : Fin n) ↦ (φ : (a : R) → R') (w i)) i j : R')
    (((φ.mapMatrix : RingHom.{u_1, u_3} (Matrix (Fin n) (Fin n) R) (Matrix (Fin n) (Fin n) R')) :
          (a : Matrix (Fin n) (Fin n) R) → Matrix (Fin n) (Fin n) R')
        (projVandermonde v w) i j :
      R')
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have succ : ∀
  (aux :
    ∀ (v w : Fin (n + 1) → K) (h0 : w 0 ≠ 0),
      (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j))
  (h0 : ¬w 0 ≠ 0), (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
Tactic: wlog h0 : w 0 ≠ 0 generalizing v w with aux
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
succ :
  ∀
    (aux :
      ∀ (v w : Fin (n + 1) → K) (h0 : w 0 ≠ 0),
        (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j))
    (h0 : ¬w 0 ≠ 0), (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have wlog : ∀ (v w : Fin (n + 1) → K) (h0 : w 0 ≠ 0),
  (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
Tactic: wlog h0 : w 0 ≠ 0 generalizing v w with aux
Cleared hypotheses: v, w
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux :
  ∀ (v w : Fin (n + 1) → K) (h0 : w 0 ≠ 0),
    (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have succ : ∀ (h0' : ∀ (a : Fin (n + 1)), w a = 0),
  (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
Tactic: obtain h0' | ⟨i₀, hi₀ : w i₀ ≠ 0⟩ := forall_or_exists_not (w · = 0)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux :
  ∀ (v w : Fin (n + 1) → K) (h0 : w 0 ≠ 0),
    (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
succ :
  ∀ (h0' : ∀ (a : Fin (n + 1)), w a = 0),
    (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have succ₁ : ∀ (i₀ : Fin (n + 1)) (hi₀ : w i₀ ≠ 0),
  (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
Tactic: obtain h0' | ⟨i₀, hi₀ : w i₀ ≠ 0⟩ := forall_or_exists_not (w · = 0)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux :
  ∀ (v w : Fin (n + 1) → K) (h0 : w 0 ≠ 0),
    (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
h0' : ∀ (a : Fin (n + 1)), w a = 0
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have succ : ∀ (ih : ∀ (v w : Fin 0 → K), (projVandermonde v w).det = ∏ i : Fin 0, ∏ j ∈ Ioi i, (v j * w i - v i * w j))
  (v w : Fin (HAdd.hAdd (α := ℕ) 0 1) → K)
  (aux :
    ∀ (v w : Fin (HAdd.hAdd (α := ℕ) 0 1) → K) (h0 : w 0 ≠ 0),
      (projVandermonde v w).det = ∏ i : Fin (0 + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j))
  (h0 : ¬w 0 ≠ 0) (h0' : ∀ (a : Fin (HAdd.hAdd (α := ℕ) 0 1)), w a = 0),
  (projVandermonde v w).det = ∏ i : Fin (0 + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
Tactic: obtain rfl | hne := eq_or_ne n 0
Cleared hypotheses: n, ih, v, w, aux, h0, h0'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux :
  ∀ (v w : Fin (n + 1) → K) (h0 : w 0 ≠ 0),
    (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
h0' : ∀ (a : Fin (n + 1)), w a = 0
succ :
  ∀ (ih : ∀ (v w : Fin 0 → K), (projVandermonde v w).det = ∏ i : Fin 0, ∏ j ∈ Ioi i, (v j * w i - v i * w j))
    (v w : Fin (HAdd.hAdd (α := ℕ) 0 1) → K)
    (aux :
      ∀ (v w : Fin (HAdd.hAdd (α := ℕ) 0 1) → K) (h0 : w 0 ≠ 0),
        (projVandermonde v w).det = ∏ i : Fin (0 + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j))
    (h0 : ¬w 0 ≠ 0) (h0' : ∀ (a : Fin (HAdd.hAdd (α := ℕ) 0 1)), w a = 0),
    (projVandermonde v w).det = ∏ i : Fin (0 + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have succ₁ : ∀ (hne : n ≠ 0), (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
Tactic: obtain rfl | hne := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux :
  ∀ (v w : Fin (n + 1) → K) (h0 : w 0 ≠ 0),
    (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
h0' : ∀ (a : Fin (n + 1)), w a = 0
hne : n ≠ 0
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have succ : Eq.{u_2 + 1} (α := K) 0 (∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j))
Tactic: rw [det_eq_zero_of_column_eq_zero 0 (fun i ↦ by simpa [projVandermonde_apply, h0']),
        Finset.prod_sigma', Finset.prod_eq_zero (i := ⟨0, Fin.last n⟩) (by simpa) (by simp [h0'])]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux :
  ∀ (v w : Fin (n + 1) → K) (h0 : w 0 ≠ 0),
    (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
h0' : ∀ (a : Fin (n + 1)), w a = 0
hne : n ≠ 0
succ : Eq.{u_2 + 1} (α := K) 0 (∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j))
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have succ₁ : Eq.{u_2 + 1} (α := K) 0
  (∏ x ∈ Finset.sigma (α := fun (a : Fin (n + 1)) ↦ Fin (n + 1)) univ Ioi,
    (v (x.snd (β := fun (i : Fin (n + 1)) ↦ Fin (n + 1))) * w (x.fst (β := fun (i : Fin (n + 1)) ↦ Fin (n + 1))) -
      v (x.fst (β := fun (i : Fin (n + 1)) ↦ Fin (n + 1))) * w (x.snd (β := fun (i : Fin (n + 1)) ↦ Fin (n + 1)))))
Tactic: rw [det_eq_zero_of_column_eq_zero 0 (fun i ↦ by simpa [projVandermonde_apply, h0']),
        Finset.prod_sigma', Finset.prod_eq_zero (i := ⟨0, Fin.last n⟩) (by simpa) (by simp [h0'])]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux :
  ∀ (v w : Fin (n + 1) → K) (h0 : w 0 ≠ 0),
    (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
h0' : ∀ (a : Fin (n + 1)), w a = 0
hne : n ≠ 0
succ : Eq.{u_2 + 1} (α := K) 0 (∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j))
succ₁ :
  Eq.{u_2 + 1} (α := K) 0
    (∏ x ∈ Finset.sigma (α := fun (a : Fin (n + 1)) ↦ Fin (n + 1)) univ Ioi,
      (v (x.snd (β := fun (i : Fin (n + 1)) ↦ Fin (n + 1))) * w (x.fst (β := fun (i : Fin (n + 1)) ↦ Fin (n + 1))) -
        v (x.fst (β := fun (i : Fin (n + 1)) ↦ Fin (n + 1))) * w (x.snd (β := fun (i : Fin (n + 1)) ↦ Fin (n + 1)))))
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have succ₂ : Eq.{u_2 + 1} (α := K) 0 0
Tactic: rw [det_eq_zero_of_column_eq_zero 0 (fun i ↦ by simpa [projVandermonde_apply, h0']),
        Finset.prod_sigma', Finset.prod_eq_zero (i := ⟨0, Fin.last n⟩) (by simpa) (by simp [h0'])]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux :
  ∀ (v w : Fin (n + 1) → K) (h0 : w 0 ≠ 0),
    (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
i₀ : Fin (n + 1)
hi₀ : w i₀ ≠ 0
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have succ : Eq.{u_2 + 1} (α := K)
  (∏ i : Fin (n + 1),
    ∏ j ∈ Ioi i,
      ((v ∘ (⇑(swap 0 i₀) : (a : Fin (n + 1)) → Fin (n + 1))) j *
          (w ∘ (⇑(swap 0 i₀) : (a : Fin (n + 1)) → Fin (n + 1))) i -
        (v ∘ (⇑(swap 0 i₀) : (a : Fin (n + 1)) → Fin (n + 1))) i *
          (w ∘ (⇑(swap 0 i₀) : (a : Fin (n + 1)) → Fin (n + 1))) j))
  (∏ i : Fin (n + 1),
    ∏ j ∈ Ioi i,
      (v ((swap 0 i₀ : (a : Fin (n + 1)) → Fin (n + 1)) j) * w ((swap 0 i₀ : (a : Fin (n + 1)) → Fin (n + 1)) i) -
        v ((swap 0 i₀ : (a : Fin (n + 1)) → Fin (n + 1)) i) * w ((swap 0 i₀ : (a : Fin (n + 1)) → Fin (n + 1)) j)))
Tactic: rw [← mul_right_inj' (a := ((Equiv.swap 0 i₀).sign : K))
      (by simp [show 0 ≠ i₀ by rintro rfl; contradiction]), ← det_permute, ← projVandermonde_comp,
      aux _ _ (by simpa), ← (Equiv.swap 0 i₀).prod_Ioi_comp_eq_sign_mul_prod (by simp)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (hypothesis)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have hr : let r := v 0 / w 0;
r = v 0 / w 0
Tactic: set r := v 0 / w 0 with hr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  (of : (a : Fin (n + 1) → Fin (n + 1) → K) → Matrix (Fin (n + 1)) (Fin (n + 1)) K) fun (i : Fin (n + 1)) ↦
    Fin.cons (α := fun (a : Fin (n + 1)) ↦ K) (projVandermonde v w i 0) fun (j : Fin n) ↦
      projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
⊢ W.submatrix succ succ =
    (of : (a : Fin n → Fin n → K) → Matrix (Fin n) (Fin n) K) fun (i j : Fin n) ↦
      (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
have a : ∀ (i j : Fin n),
  W.submatrix succ succ i j =
    (of : (a : Fin n → Fin n → K) → Matrix (Fin n) (Fin n) K)
      (fun (i j : Fin n) ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  (of : (a : Fin (n + 1) → Fin (n + 1) → K) → Matrix (Fin (n + 1)) (Fin (n + 1)) K) fun (i : Fin (n + 1)) ↦
    Fin.cons (α := fun (a : Fin (n + 1)) ↦ K) (projVandermonde v w i 0) fun (j : Fin n) ↦
      projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
i j : Fin n
⊢ W.submatrix succ succ i j =
    (of : (a : Fin n → Fin n → K) → Matrix (Fin n) (Fin n) K)
      (fun (i j : Fin n) ↦ (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j) i j
have a : Eq.{u_2 + 1} (α := K)
  ((of : (a : Fin (n + 1) → Fin (n + 1) → K) → Matrix (Fin (n + 1)) (Fin (n + 1)) K)
      (fun (i : Fin (n + 1)) ↦
        Fin.cons (α := fun (a : Fin (n + 1)) ↦ K) (HPow.hPow (β := ℕ) (v i) 0 * w i ^ n) fun (j : Fin n) ↦
          v i ^ ((↑j : ℕ) + 1) * w i ^ (↑j.rev : ℕ) - v 0 / w 0 * (v i ^ (↑j : ℕ) * w i ^ ((↑j.rev : ℕ) + 1)))
      i.succ j.succ :
    K)
  ((of : (a : Fin n → Fin n → K) → Matrix (Fin n) (Fin n) K)
      (fun (i j : Fin n) ↦ (v i.succ - v 0 / w 0 * w i.succ) * (v i.succ ^ (↑j : ℕ) * w i.succ ^ (↑j.rev : ℕ))) i j :
    K)
Tactic: simp only [projVandermonde_apply, val_zero, rev_zero, val_last, val_succ,
      val_castSucc, submatrix_apply, Function.comp_apply, rev_succ,
      W, r, rev_castSucc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  (of : (a : Fin (n + 1) → Fin (n + 1) → K) → Matrix (Fin (n + 1)) (Fin (n + 1)) K) fun (i : Fin (n + 1)) ↦
    Fin.cons (α := fun (a : Fin (n + 1)) ↦ K) (projVandermonde v w i 0) fun (j : Fin n) ↦
      projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
i j : Fin n
⊢ Eq.{u_2 + 1} (α := K)
    ((of : (a : Fin (n + 1) → Fin (n + 1) → K) → Matrix (Fin (n + 1)) (Fin (n + 1)) K)
        (fun (i : Fin (n + 1)) ↦
          Fin.cons (α := fun (a : Fin (n + 1)) ↦ K) (HPow.hPow (β := ℕ) (v i) 0 * w i ^ n) fun (j : Fin n) ↦
            v i ^ ((↑j : ℕ) + 1) * w i ^ (↑j.rev : ℕ) - v 0 / w 0 * (v i ^ (↑j : ℕ) * w i ^ ((↑j.rev : ℕ) + 1)))
        i.succ j.succ :
      K)
    ((of : (a : Fin n → Fin n → K) → Matrix (Fin n) (Fin n) K)
        (fun (i j : Fin n) ↦ (v i.succ - v 0 / w 0 * w i.succ) * (v i.succ ^ (↑j : ℕ) * w i.succ ^ (↑j.rev : ℕ))) i j :
      K)
have a : v i.succ ^ ((↑j : ℕ) + 1) * w i.succ ^ (n - ((↑j : ℕ) + 1)) -
    v 0 / w 0 * (v i.succ ^ (↑j : ℕ) * w i.succ ^ (n - ((↑j : ℕ) + 1) + 1)) =
  (v i.succ - v 0 / w 0 * w i.succ) * (v i.succ ^ (↑j : ℕ) * w i.succ ^ (n - ((↑j : ℕ) + 1)))
Tactic: simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (hypothesis)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  (of : (a : Fin (n + 1) → Fin (n + 1) → K) → Matrix (Fin (n + 1)) (Fin (n + 1)) K) fun (i : Fin (n + 1)) ↦
    Fin.cons (α := fun (a : Fin (n + 1)) ↦ K) (projVandermonde v w i 0) fun (j : Fin n) ↦
      projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have hW_eq : W.submatrix succ succ =
  (of : (a : Fin n → Fin n → K) → Matrix (Fin n) (Fin n) K) fun (i j : Fin n) ↦
    (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
Tactic: have hW_eq : (W.submatrix succ succ) = .of fun i j ↦ (v (succ i) - r * w (succ i)) *
      projVandermonde (v ∘ succ) (w ∘ succ) i j := by
    ext i j
    simp only [projVandermonde_apply, val_zero, rev_zero, val_last, val_succ,
      val_castSucc, submatrix_apply, Function.comp_apply, rev_succ,
      W, r, rev_castSucc]
    simp
    ring
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  (of : (a : Fin (n + 1) → Fin (n + 1) → K) → Matrix (Fin (n + 1)) (Fin (n + 1)) K) fun (i : Fin (n + 1)) ↦
    Fin.cons (α := fun (a : Fin (n + 1)) ↦ K) (projVandermonde v w i 0) fun (j : Fin n) ↦
      projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq :
  W.submatrix succ succ =
    (of : (a : Fin n → Fin n → K) → Matrix (Fin n) (Fin n) K) fun (i j : Fin n) ↦
      (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have rw : HPow.hPow (α := K) (-1) (↑0 : ℕ) * W 0 0 * (W.submatrix succ (succAbove 0)).det =
  ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
Tactic: rw [det_eq_of_forall_col_eq_smul_add_pred (B := W) (c := fun _ ↦ r) (by simp [W])
    (fun i j ↦ by simp [W, r, projVandermonde_apply]), det_succ_row_zero,
    Finset.sum_eq_single 0 _ (by simp)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  (of : (a : Fin (n + 1) → Fin (n + 1) → K) → Matrix (Fin (n + 1)) (Fin (n + 1)) K) fun (i : Fin (n + 1)) ↦
    Fin.cons (α := fun (a : Fin (n + 1)) ↦ K) (projVandermonde v w i 0) fun (j : Fin n) ↦
      projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq :
  W.submatrix succ succ =
    (of : (a : Fin n → Fin n → K) → Matrix (Fin n) (Fin n) K) fun (i j : Fin n) ↦
      (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
rw :
  HPow.hPow (α := K) (-1) (↑0 : ℕ) * W 0 0 * (W.submatrix succ (succAbove 0)).det =
    ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have rw₁ : ∀ (b : Fin n.succ),
  Membership.mem (γ := Finset (Fin n.succ)) univ b →
    b ≠ 0 → HPow.hPow (α := K) (-1) (↑b : ℕ) * W 0 b * (W.submatrix succ b.succAbove).det = 0
Tactic: rw [det_eq_of_forall_col_eq_smul_add_pred (B := W) (c := fun _ ↦ r) (by simp [W])
    (fun i j ↦ by simp [W, r, projVandermonde_apply]), det_succ_row_zero,
    Finset.sum_eq_single 0 _ (by simp)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  (of : (a : Fin (n + 1) → Fin (n + 1) → K) → Matrix (Fin (n + 1)) (Fin (n + 1)) K) fun (i : Fin (n + 1)) ↦
    Fin.cons (α := fun (a : Fin (n + 1)) ↦ K) (projVandermonde v w i 0) fun (j : Fin n) ↦
      projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq :
  W.submatrix succ succ =
    (of : (a : Fin n → Fin n → K) → Matrix (Fin n) (Fin n) K) fun (i j : Fin n) ↦
      (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ HPow.hPow (α := K) (-1) (↑0 : ℕ) * W 0 0 * (W.submatrix succ (succAbove 0)).det =
    ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have rw : HPow.hPow (α := K) (-1) (↑0 : ℕ) * W 0 0 *
    HMul.hMul (α := K) (∏ i : Fin n, (v i.succ - r * w i.succ))
      (∏ i : Fin n, ∏ j ∈ Ioi i, ((v ∘ succ) j * (w ∘ succ) i - (v ∘ succ) i * (w ∘ succ) j)) =
  ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
Tactic: rw [succAbove_zero, hW_eq, det_mul_column, ih]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  (of : (a : Fin (n + 1) → Fin (n + 1) → K) → Matrix (Fin (n + 1)) (Fin (n + 1)) K) fun (i : Fin (n + 1)) ↦
    Fin.cons (α := fun (a : Fin (n + 1)) ↦ K) (projVandermonde v w i 0) fun (j : Fin n) ↦
      projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq :
  W.submatrix succ succ =
    (of : (a : Fin n → Fin n → K) → Matrix (Fin n) (Fin n) K) fun (i j : Fin n) ↦
      (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ HPow.hPow (α := K) (-1) (↑0 : ℕ) * W 0 0 *
      HMul.hMul (α := K) (∏ i : Fin n, (v i.succ - r * w i.succ))
        (∏ i : Fin n, ∏ j ∈ Ioi i, ((v ∘ succ) j * (w ∘ succ) i - (v ∘ succ) i * (w ∘ succ) j)) =
    ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have simp : w 0 ^ n *
    HMul.hMul (α := K) (∏ x : Fin n, (v x.succ - v 0 / w 0 * w x.succ))
      (∏ i : Fin n, ∏ j ∈ Ioi i, ((v ∘ succ) j * (w ∘ succ) i - (v ∘ succ) i * (w ∘ succ) j)) =
  ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
Tactic: simp only [Nat.succ_eq_add_one, coe_ofNat_eq_mod, Nat.zero_mod,
      pow_zero, show W 0 0 = w 0 ^ n by simp [W, projVandermonde_apply], one_mul, hr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  (of : (a : Fin (n + 1) → Fin (n + 1) → K) → Matrix (Fin (n + 1)) (Fin (n + 1)) K) fun (i : Fin (n + 1)) ↦
    Fin.cons (α := fun (a : Fin (n + 1)) ↦ K) (projVandermonde v w i 0) fun (j : Fin n) ↦
      projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq :
  W.submatrix succ succ =
    (of : (a : Fin n → Fin n → K) → Matrix (Fin n) (Fin n) K) fun (i j : Fin n) ↦
      (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ w 0 ^ n *
      HMul.hMul (α := K) (∏ x : Fin n, (v x.succ - v 0 / w 0 * w x.succ))
        (∏ i : Fin n, ∏ j ∈ Ioi i, ((v ∘ succ) j * (w ∘ succ) i - (v ∘ succ) i * (w ∘ succ) j)) =
    ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have field_simp : (w 0 ^ n * ∏ x : Fin n, (v x.succ * w 0 - v 0 * w x.succ) / w 0) *
    ∏ x : Fin n, ∏ x_1 ∈ Ioi x, ((v ∘ succ) x_1 * (w ∘ succ) x - (v ∘ succ) x * (w ∘ succ) x_1) =
  ∏ x : Fin (n + 1), ∏ x_1 ∈ Ioi x, (v x_1 * w x - v x * w x_1)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n_1 n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
h0 : w 0 ≠ 0
r : K := v 0 / w 0
hr : r = v 0 / w 0
W : Matrix (Fin (n + 1)) (Fin (n + 1)) K :=
  (of : (a : Fin (n + 1) → Fin (n + 1) → K) → Matrix (Fin (n + 1)) (Fin (n + 1)) K) fun (i : Fin (n + 1)) ↦
    Fin.cons (α := fun (a : Fin (n + 1)) ↦ K) (projVandermonde v w i 0) fun (j : Fin n) ↦
      projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc
hW_eq :
  W.submatrix succ succ =
    (of : (a : Fin n → Fin n → K) → Matrix (Fin n) (Fin n) K) fun (i j : Fin n) ↦
      (v i.succ - r * w i.succ) * projVandermonde (v ∘ succ) (w ∘ succ) i j
⊢ (w 0 ^ n * ∏ x : Fin n, (v x.succ * w 0 - v 0 * w x.succ) / w 0) *
      ∏ x : Fin n, ∏ x_1 ∈ Ioi x, ((v ∘ succ) x_1 * (w ∘ succ) x - (v ∘ succ) x * (w ∘ succ) x_1) =
    ∏ x : Fin (n + 1), ∏ x_1 ∈ Ioi x, (v x_1 * w x - v x * w x_1)
have simp : w 0 ^ n * ((∏ x : Fin n, (v x.succ * w 0 - v 0 * w x.succ)) / w 0 ^ n) *
    ∏ x : Fin n, ∏ x_1 ∈ Ioi x, (v x_1.succ * w x.succ - v x.succ * w x_1.succ) =
  ∏ x : Fin (n + 1), ∏ x_1 ∈ Ioi x, (v x_1 * w x - v x * w x_1)
Tactic: simp only [Finset.prod_div_distrib, Finset.prod_const, Finset.card_fin, Function.comp_apply]