awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
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)
⊢ 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:
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]

Premises used: Fin.val_succ, Fin.rev_castSucc, Function.comp_apply, Matrix.submatrix_apply, Matrix.projVandermonde_apply, Fin.rev_succ, Fin.val_zero, Fin.rev_zero, Fin.val_last, Fin.val_castSucc
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
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)))
⊢ 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
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
⊢ 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:
ring
-- Module: Mathlib.LinearAlgebra.Vandermonde
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

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
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
⊢ ∀ (i : Fin (n + 1)), projVandermonde v w i 0 = W i 0

Tactic:
simp [W]
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
i : Fin (n + 1)
j : Fin n
⊢ projVandermonde v w i j.succ = W i j.succ + (fun (x : Fin n) ↦ r) j * projVandermonde v w i j.castSucc

Tactic:
simp [W, r, projVandermonde_apply]

Premises used: Matrix.projVandermonde_apply
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
⊢ 0 ∉ univ → HPow.hPow (α := K) (-1) (↑0 : ℕ) * W 0 0 * (W.submatrix succ (succAbove 0)).det = 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Vandermonde
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)
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
⊢ (projVandermonde v w).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)]

Premises used: Finset.sum_eq_single, OfNat.ofNat, Matrix.det_succ_row_zero, Matrix.det_eq_of_forall_col_eq_smul_add_pred
-- Module: Mathlib.LinearAlgebra.Vandermonde
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 *
      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)
⊢ 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 [succAbove_zero, hW_eq, det_mul_column, ih]

Premises used: Matrix.det_mul_column, Fin.succAbove_zero
-- Module: Mathlib.LinearAlgebra.Vandermonde
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 0 = w 0 ^ n

Tactic:
simp [W, projVandermonde_apply]

Premises used: Matrix.projVandermonde_apply
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
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)
⊢ 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:
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]

Premises used: Nat.succ_eq_add_one, pow_zero, Fin.coe_ofNat_eq_mod, Nat.zero_mod, one_mul
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
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)
⊢ 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:
field_simp
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
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)
⊢ (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:
simp only [Finset.prod_div_distrib, Finset.prod_const, Finset.card_fin, Function.comp_apply]

Premises used: Finset.prod_const, Finset.card_fin, Function.comp_apply, Finset.prod_div_distrib
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
field_simp :
  HMul.hMul (α := K) (∏ x : Fin n, (w 0 * v x.succ - v 0 * w x.succ))
      (∏ x : Fin n, ∏ x_1 ∈ Ioi x, (w x.succ * v x_1.succ - v x.succ * w x_1.succ)) =
    ∏ x : Fin (n + 1), ∏ x_1 ∈ Ioi x, (w x * v x_1 - v x * w x_1)
⊢ 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:
field_simp
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
⊢ HMul.hMul (α := K) (∏ x : Fin n, (w 0 * v x.succ - v 0 * w x.succ))
      (∏ x : Fin n, ∏ x_1 ∈ Ioi x, (w x.succ * v x_1.succ - v x.succ * w x_1.succ)) =
    ∏ x : Fin (n + 1), ∏ x_1 ∈ Ioi x, (w x * v x_1 - v x * w x_1)

Tactic:
simp only [prod_univ_succ, Ioi_zero_eq_map, Finset.prod_map, coe_succEmb, prod_Ioi_succ]

Premises used: Fin.coe_succEmb, Fin.prod_Ioi_succ, Fin.prod_univ_succ, Finset.prod_map, Fin.Ioi_zero_eq_map
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
j : Fin n.succ
_ :
  Membership.mem (γ := Finset (Fin n.succ)) univ j →
    j ≠ 0 → HPow.hPow (α := K) (-1) (↑j : ℕ) * W 0 j * (W.submatrix succ j.succAbove).det = 0
⊢ Membership.mem (γ := Finset (Fin n.succ)) univ j →
    j ≠ 0 → HPow.hPow (α := K) (-1) (↑j : ℕ) * W 0 j * (W.submatrix succ j.succAbove).det = 0

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
j : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ j
hj0 : j ≠ 0
obtain :
  ∀ (j : Fin n),
    Membership.mem (γ := Finset (Fin n.succ)) univ j.succ →
      ∀ (hj0 : j.succ ≠ 0),
        HPow.hPow (α := K) (-1) (↑j.succ : ℕ) * W 0 j.succ * (W.submatrix succ j.succ.succAbove).det = 0
⊢ HPow.hPow (α := K) (-1) (↑j : ℕ) * W 0 j * (W.submatrix succ j.succAbove).det = 0

Tactic:
obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero hj0

Premises used: Fin.eq_succ_of_ne_zero, rfl
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
j : Fin n
h : Membership.mem (γ := Finset (Fin n.succ)) univ j.succ
hj0 : j.succ ≠ 0
rw : (HPow.hPow (α := K) (-1) (↑j.succ : ℕ) = 0 ∨ W 0 j.succ = 0) ∨ (W.submatrix succ j.succ.succAbove).det = 0
⊢ HPow.hPow (α := K) (-1) (↑j.succ : ℕ) * W 0 j.succ * (W.submatrix succ j.succ.succAbove).det = 0

Tactic:
rw [mul_eq_zero, mul_eq_zero]

Premises used: mul_eq_zero
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
j : Fin n
h : Membership.mem (γ := Finset (Fin n.succ)) univ j.succ
hj0 : j.succ ≠ 0
⊢ (HPow.hPow (α := K) (-1) (↑j.succ : ℕ) = 0 ∨ W 0 j.succ = 0) ∨ (W.submatrix succ j.succ.succAbove).det = 0

Tactic:
.inl (.inr ?_)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
j : Fin n
h : Membership.mem (γ := Finset (Fin n.succ)) univ j.succ
hj0 : j.succ ≠ 0
refine : W 0 j.succ = 0
⊢ (HPow.hPow (α := K) (-1) (↑j.succ : ℕ) = 0 ∨ W 0 j.succ = 0) ∨ (W.submatrix succ j.succ.succAbove).det = 0

Tactic:
refine .inl (.inr ?_)