awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n.succ → R
rw :
  Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v 0 ^ (↑j : ℕ)) fun (i : Fin n) ↦
    Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦
      tail (α := fun (i : Fin (n + 1)) ↦ R) v i * vandermonde (tail (α := fun (i : Fin (n + 1)) ↦ R) v) i j
| vandermonde v

Tactic:
rw [← Fin.cons_self_tail v, vandermonde_cons]

Premises used: Fin.cons_self_tail, Matrix.vandermonde_cons
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n.succ → R
conv_lhs :
  Eq.{u_1 + 1} (α := Matrix (Fin n.succ) (Fin n.succ) R)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v 0 ^ (↑j : ℕ)) fun (i : Fin n) ↦
      Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦
        tail (α := fun (i : Fin (n + 1)) ↦ R) v i * vandermonde (tail (α := fun (i : Fin (n + 1)) ↦ R) v) i j)
    ((of :
        (a : (Fin n.succ → R) → ((i : Fin n) → Fin n.succ → R) → (i : Fin (n + 1)) → Fin n.succ → R) →
          Matrix (Fin n.succ → R) ((i : Fin n) → Fin n.succ → R) ((i : Fin (n + 1)) → Fin n.succ → R))
      (Fin.cons (α := fun (a : Fin n.succ) ↦ Fin n.succ → R) :
        (x : Fin n.succ → R) → (p : (i : Fin n) → Fin n.succ → R) → (i : Fin (n + 1)) → Fin n.succ → R)
      (fun (j : Fin n.succ) ↦ v 0 ^ (↑j : ℕ)) fun (i : Fin n) ↦
      Fin.cons (α := fun (a : Fin n.succ) ↦ R) 1 fun (j : Fin n) ↦
        v i.succ * vandermonde (tail (α := fun (i : Fin (n + 1)) ↦ R) v) i j)
⊢ vandermonde v =
    (of :
        (a : (Fin n.succ → R) → ((i : Fin n) → Fin n.succ → R) → (i : Fin (n + 1)) → Fin n.succ → R) →
          Matrix (Fin n.succ → R) ((i : Fin n) → Fin n.succ → R) ((i : Fin (n + 1)) → Fin n.succ → R))
      (Fin.cons (α := fun (a : Fin n.succ) ↦ Fin n.succ → R) :
        (x : Fin n.succ → R) → (p : (i : Fin n) → Fin n.succ → R) → (i : Fin (n + 1)) → Fin n.succ → R)
      (fun (j : Fin n.succ) ↦ v 0 ^ (↑j : ℕ)) fun (i : Fin n) ↦
      Fin.cons (α := fun (a : Fin n.succ) ↦ R) 1 fun (j : Fin n) ↦
        v i.succ * vandermonde (tail (α := fun (i : Fin (n + 1)) ↦ R) v) i j

Tactic:
conv_lhs => rw [← Fin.cons_self_tail v, vandermonde_cons]

Premises used: Fin.cons_self_tail, Matrix.vandermonde_cons
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n.succ → R
⊢ Eq.{u_1 + 1} (α := Matrix (Fin n.succ) (Fin n.succ) R)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v 0 ^ (↑j : ℕ)) fun (i : Fin n) ↦
      Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦
        tail (α := fun (i : Fin (n + 1)) ↦ R) v i * vandermonde (tail (α := fun (i : Fin (n + 1)) ↦ R) v) i j)
    ((of :
        (a : (Fin n.succ → R) → ((i : Fin n) → Fin n.succ → R) → (i : Fin (n + 1)) → Fin n.succ → R) →
          Matrix (Fin n.succ → R) ((i : Fin n) → Fin n.succ → R) ((i : Fin (n + 1)) → Fin n.succ → R))
      (Fin.cons (α := fun (a : Fin n.succ) ↦ Fin n.succ → R) :
        (x : Fin n.succ → R) → (p : (i : Fin n) → Fin n.succ → R) → (i : Fin (n + 1)) → Fin n.succ → R)
      (fun (j : Fin n.succ) ↦ v 0 ^ (↑j : ℕ)) fun (i : Fin n) ↦
      Fin.cons (α := fun (a : Fin n.succ) ↦ R) 1 fun (j : Fin n) ↦
        v i.succ * vandermonde (tail (α := fun (i : Fin (n + 1)) ↦ R) v) i j)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin n → R
i j : Fin n
⊢ (vandermonde v * (vandermonde w)ᵀ) i j = ∑ k : Fin n, (v i * w j) ^ (↑k : ℕ)

Tactic:
simp only [vandermonde_apply, Matrix.mul_apply, Matrix.transpose_apply, mul_pow]

Premises used: Matrix.mul_apply, Matrix.vandermonde_apply, Matrix.transpose_apply, mul_pow
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
i j : Fin n
⊢ ((vandermonde v)ᵀ * vandermonde v) i j = ∑ k : Fin n, v k ^ ((↑i : ℕ) + (↑j : ℕ))

Tactic:
simp only [vandermonde_apply, Matrix.mul_apply, Matrix.transpose_apply, pow_add]

Premises used: pow_add, Matrix.mul_apply, Matrix.vandermonde_apply, Matrix.transpose_apply
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
hw : w i = 0
h :
  ∀ (j : Fin (n + 1)), rectVandermonde v w (n + 1) i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j
⊢ rectVandermonde v w (n + 1) i = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n)

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
hw : w i = 0
j : Fin (n + 1)
h : rectVandermonde v w (n + 1) i (last n) = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) (last n)
h₁ :
  ∀ (hlt : j < last n),
    rectVandermonde v w (n + 1) i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j
⊢ rectVandermonde v w (n + 1) i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j

Tactic:
obtain rfl | hlt := j.le_last.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl, Fin.le_last
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
hw : w i = 0
⊢ rectVandermonde v w (n + 1) i (last n) = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) (last n)

Tactic:
simp [rectVandermonde_apply]

Premises used: Matrix.rectVandermonde_apply
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
hw : w i = 0
j : Fin (n + 1)
hlt : j < last n
h : (↑j.rev : ℕ) ≠ 0
⊢ rectVandermonde v w (n + 1) i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j

Tactic:
rw [rectVandermonde_apply, Pi.single_eq_of_ne hlt.ne, hw, zero_pow, mul_zero]

Premises used: Pi.single_eq_of_ne, MulZeroClass.mul_zero, Matrix.rectVandermonde_apply, zero_pow, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
hw : w i = 0
j : Fin (n + 1)
hlt : j < last n
⊢ (↑j.rev : ℕ) ≠ 0

Tactic:
simpa [Nat.sub_eq_zero_iff_le] using hlt

Premises used: Nat.sub_eq_zero_iff_le
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
K : Type u_2
inst : Field K
n : ℕ
v w : Fin (n + 1) → K
i j : Fin (n + 1)
hw : w i ≠ 0
⊢ w i ^ (↑j : ℕ) ≠ 0

Tactic:
simp [hw]
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
K : Type u_2
inst : Field K
n : ℕ
v w : Fin (n + 1) → K
i j : Fin (n + 1)
hw : w i ≠ 0
rw : v i ^ (↑j : ℕ) * w i ^ (↑j.rev : ℕ) = v i ^ (↑j : ℕ) * w i ^ n / w i ^ (↑j : ℕ)
rw₁ : v i ^ (↑j : ℕ) * w i ^ (↑j.rev : ℕ) * w i ^ (↑j : ℕ) = v i ^ (↑j : ℕ) * w i ^ n
rw₂ : v i ^ (↑j : ℕ) * (w i ^ (↑j.rev : ℕ) * w i ^ (↑j : ℕ)) = v i ^ (↑j : ℕ) * w i ^ n
rw₃ : v i ^ (↑j : ℕ) * w i ^ ((↑j.rev : ℕ) + (↑j : ℕ)) = v i ^ (↑j : ℕ) * w i ^ n
rw₄ rw₅ : v i ^ (↑j : ℕ) * w i ^ n = v i ^ (↑j : ℕ) * w i ^ n
⊢ projVandermonde v w i j = v i ^ (↑j : ℕ) * w i ^ n / w i ^ (↑j : ℕ)

Tactic:
rw [projVandermonde_apply, eq_div_iff (by simp [hw]), mul_assoc, ← pow_add, rev_add_cast]

Premises used: mul_assoc, pow_add, Fin.rev_add_cast, Matrix.projVandermonde_apply, eq_div_iff
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin (n + 1) → R
i : Fin (n + 1)
hw : w i = 0
h : ∀ (j : Fin (n + 1)), projVandermonde v w i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j
⊢ projVandermonde v w i = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n)

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin (n + 1) → R
i : Fin (n + 1)
hw : w i = 0
j : Fin (n + 1)
h : projVandermonde v w i (last n) = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) (last n)
h₁ : ∀ (hlt : j < last n), projVandermonde v w i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j
⊢ projVandermonde v w i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j

Tactic:
obtain rfl | hlt := j.le_last.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl, Fin.le_last
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin (n + 1) → R
i : Fin (n + 1)
hw : w i = 0
⊢ projVandermonde v w i (last n) = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) (last n)

Tactic:
simp [projVandermonde_apply]

Premises used: Matrix.projVandermonde_apply
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin (n + 1) → R
i : Fin (n + 1)
hw : w i = 0
j : Fin (n + 1)
hlt : j < last n
h : (↑j.rev : ℕ) ≠ 0
⊢ projVandermonde v w i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j

Tactic:
rw [projVandermonde_apply, Pi.single_eq_of_ne hlt.ne, hw, zero_pow, mul_zero]

Premises used: Pi.single_eq_of_ne, MulZeroClass.mul_zero, Matrix.projVandermonde_apply, zero_pow, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin (n + 1) → R
i : Fin (n + 1)
hw : w i = 0
j : Fin (n + 1)
hlt : j < last n
⊢ (↑j.rev : ℕ) ≠ 0

Tactic:
simpa [Nat.sub_eq_zero_iff_le] using hlt

Premises used: Nat.sub_eq_zero_iff_le
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin n → R
f : Fin n → Fin n
⊢ projVandermonde (v ∘ f) (w ∘ f) = (projVandermonde v w).submatrix f id

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.projVandermonde, rfl, Matrix.rectVandermonde
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
R' : Type u_3
inst_1 : CommRing R'
φ : R →+* R'
v w : Fin n → R
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')
⊢ 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))

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
R' : Type u_3
inst_1 : CommRing R'
φ : R →+* R'
v w : Fin n → R
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:
simp [projVandermonde_apply]

Premises used: Matrix.projVandermonde_apply
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
K : Type u_2
inst : Field K
n : ℕ
v w : Fin 0 → K
⊢ (projVandermonde v w).det = ∏ i : Fin 0, ∏ j ∈ Ioi i, (v j * w i - v i * w j)

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
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)
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)
⊢ (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

Premises used: OfNat.ofNat
-- 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
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)
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)
⊢ (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)

Premises used: forall_or_exists_not, OfNat.ofNat, Eq
-- 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
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)
succ₁ : ∀ (hne : n ≠ 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)

Tactic:
obtain rfl | hne := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
K : Type u_2
inst : Field K
n : ℕ
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:
simp [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
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
i : Fin (n + 1)
⊢ projVandermonde v w i 0 = 0

Tactic:
simpa [projVandermonde_apply, h0']

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
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
⊢ Membership.mem (γ := Finset ((_ : Fin (n + 1)) × Fin (n + 1)))
    (Finset.sigma (α := fun (a : Fin (n + 1)) ↦ Fin (n + 1)) univ Ioi)
    (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ Fin (n + 1)) 0 (last n))

Tactic:
simpa
-- 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
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
⊢ v ((Sigma.mk (β := fun (i : Fin (n + 1)) ↦ Fin (n + 1)) 0 (last n)).snd (β := fun (i : Fin (n + 1)) ↦ Fin (n + 1))) *
        w
          ((Sigma.mk (β := fun (i : Fin (n + 1)) ↦ Fin (n + 1)) 0 (last n)).fst (β := fun (i : Fin (n + 1)) ↦
            Fin (n + 1))) -
      v
          ((Sigma.mk (β := fun (i : Fin (n + 1)) ↦ Fin (n + 1)) 0 (last n)).fst (β := fun (i : Fin (n + 1)) ↦
            Fin (n + 1))) *
        w
          ((Sigma.mk (β := fun (i : Fin (n + 1)) ↦ Fin (n + 1)) 0 (last n)).snd (β := fun (i : Fin (n + 1)) ↦
            Fin (n + 1))) =
    0

Tactic:
simp [h0']
-- 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
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)))))
succ₂ succ₃ : Eq.{u_2 + 1} (α := K) 0 0
⊢ (projVandermonde v w).det = ∏ 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'])]

Premises used: Finset.prod_eq_zero, Finset.prod_sigma', Matrix.det_eq_zero_of_column_eq_zero, OfNat.ofNat
-- 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
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
hi₀ : w 0 ≠ 0
⊢ False

Tactic:
contradiction
-- 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
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
⊢ Ne.{u_2 + 1} (α := K) (↑(↑((Perm.sign : (a : Perm (Fin (n + 1))) → ℤˣ) (swap 0 i₀)) : ℤ) : K) 0

Tactic:
simp [show 0 ≠ i₀ by rintro rfl; contradiction]
-- 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
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
⊢ Function.comp (α := Fin (n + 1)) w (⇑(swap 0 i₀) : (a : Fin (n + 1)) → Fin (n + 1)) 0 ≠ 0

Tactic:
simpa
-- 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
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
⊢ ∀ (i j : Fin (n + 1)), v j * w i - v i * w j = -(v i * w j - v j * w i)

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
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
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)))
⊢ (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w 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)]

Premises used: Matrix.det_permute, Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod, Equiv.swap, mul_right_inj', Matrix.projVandermonde_comp, OfNat.ofNat
-- 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
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
⊢ 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:
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
⊢ let r := v 0 / w 0;
  r = v 0 / w 0

Tactic:
set r := v 0 / w 0 with hr

Premises used: OfNat.ofNat
-- 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
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
⊢ 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:
ext i j