awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ^ 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)
have 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)
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
j : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ j
hj0 : j ≠ 0
⊢ HPow.hPow (α := K) (-1) (↑j : ℕ) * W 0 j * (W.submatrix succ j.succAbove).det = 0
have 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
Tactic: obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero hj0
Cleared hypotheses: j, h, hj0
-- 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
j : Fin n
h : 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
have rw : (HPow.hPow (α := K) (-1) (↑j.succ : ℕ) = 0 ∨ W 0 j.succ = 0) ∨ (W.submatrix succ j.succ.succAbove).det = 0
Tactic: rw [mul_eq_zero, mul_eq_zero]
-- 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
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
have refine : W 0 j.succ = 0
Tactic: refine .inl (.inr ?_)
-- 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
j : Fin n
h : Membership.mem (γ := Finset (Fin n.succ)) univ j.succ
hj0 : j.succ ≠ 0
⊢ W 0 j.succ = 0
have simp : v 0 ^ ((↑j : ℕ) + 1) * w 0 ^ n / w 0 ^ ((↑j : ℕ) + 1) - v 0 / w 0 * (v 0 ^ (↑j : ℕ) * w 0 ^ n / w 0 ^ (↑j : ℕ)) = 0
Tactic: simp only [of_apply, projVandermonde_apply_of_ne_zero h0, val_succ, val_castSucc, cons_succ, W, r]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n : ℕ
v w : Fin n → K
⊢ (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have zero : ∀ (v w : Fin 0 → K), (projVandermonde v w).det = ∏ i : Fin 0, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
  /- We can assume not all `w i` are zero, and therefore that `w 0 ≠ 0`,
  since otherwise we can swap row `0` with another nonzero row. -/
  wlog h0 : w 0 ≠ 0 generalizing v w with aux
  · obtain h0' | ⟨i₀, hi₀ : w i₀ ≠ 0⟩ := forall_or_exists_not (w · = 0)
    · obtain rfl | hne := eq_or_ne n 0
      · simp [projVandermonde_apply]
      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'])]
    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)]
    rfl
  /- Let `W` be obtained from the matrix by subtracting `r = (v 0) / (w 0)` times each column
  from the next column, starting from the penultimate column. This doesn't change the determinant.-/
  set r := v 0 / w 0 with hr
  set W : Matrix (Fin (n + 1)) (Fin (n + 1)) K := .of fun i ↦ (cons (projVandermonde v w i 0)
    (fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc))
  -- deleting the first row and column of `W` gives a row-scaling of a Vandermonde matrix.
  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
  /- The first row of `W` is `[(w 0)^n, 0, ..., 0]` - take a cofactor expansion along this row,
  and apply induction. -/
  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)]
  · rw [succAbove_zero, hW_eq, det_mul_column, ih]
    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]
    field_simp
    simp only [Finset.prod_div_distrib, Finset.prod_const, Finset.card_fin, Function.comp_apply]
    field_simp
    simp only [prod_univ_succ, Ioi_zero_eq_map, Finset.prod_map, coe_succEmb, prod_Ioi_succ]
  intro j _ hj0
  obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero hj0
  rw [mul_eq_zero, mul_eq_zero]
  refine .inl (.inr ?_)
  simp only [of_apply, projVandermonde_apply_of_ne_zero h0, val_succ, val_castSucc, cons_succ, W, r]
  ring
Cleared hypotheses: v, w
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin n → R
u : (b : Bool) → (i : Fin n) → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun (b : Bool) (i : Fin n) ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ)) :
        (a : MvPolynomial (Fin n × Bool) ℤ) → FractionRing (MvPolynomial (Fin n × Bool) ℤ))
      (MvPolynomial.X (i, b))
⊢ (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have hdet : (projVandermonde (u true) (u false)).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (u true j * u false i - u true i * u false j)
Tactic: have hdet := det_projVandermonde_of_field (u true) (u false)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin n → R
u : (b : Bool) → (i : Fin n) → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun (b : Bool) (i : Fin n) ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ)) :
        (a : MvPolynomial (Fin n × Bool) ℤ) → FractionRing (MvPolynomial (Fin n × Bool) ℤ))
      (MvPolynomial.X (i, b))
hdet :
  Eq (α := FractionRing (MvPolynomial (Fin n × Bool) ℤ))
    (det (n := Fin n)
      (projVandermonde
        (fun (i : Fin n) ↦
          (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ)) :
              (a : MvPolynomial (Fin n × Bool) ℤ) → FractionRing (MvPolynomial (Fin n × Bool) ℤ))
            (MvPolynomial.X (i, true)))
        fun (i : Fin n) ↦
        (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ)) :
            (a : MvPolynomial (Fin n × Bool) ℤ) → FractionRing (MvPolynomial (Fin n × Bool) ℤ))
          (MvPolynomial.X (i, false))))
    (↑(∏ i : Fin n,
          ∏ i_1 ∈ Ioi i,
            (HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i_1, true)) (MvPolynomial.X (i, false)) -
              HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i, true))
                (MvPolynomial.X (i_1, false)))) :
      FractionRing (MvPolynomial (Fin n × Bool) ℤ))
⊢ (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have hdet₁ : Eq (α := MvPolynomial (Fin n × Bool) ℤ)
  (det (n := Fin n)
    (projVandermonde (fun (i : Fin n) ↦ MvPolynomial.X (i, true)) fun (i : Fin n) ↦ MvPolynomial.X (i, false)))
  (∏ i : Fin n,
    ∏ i_1 ∈ Ioi i,
      (HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i_1, true)) (MvPolynomial.X (i, false)) -
        HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i, true)) (MvPolynomial.X (i_1, false))))
Tactic: rw [projVandermonde_map, ← RingHom.map_det, IsFractionRing.coe_inj] at hdet
Cleared hypotheses: hdet
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin n → R
u : (b : Bool) → (i : Fin n) → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun (b : Bool) (i : Fin n) ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ)) :
        (a : MvPolynomial (Fin n × Bool) ℤ) → FractionRing (MvPolynomial (Fin n × Bool) ℤ))
      (MvPolynomial.X (i, b))
hdet :
  Eq (α := MvPolynomial (Fin n × Bool) ℤ)
    (det (n := Fin n)
      (projVandermonde (fun (i : Fin n) ↦ MvPolynomial.X (i, true)) fun (i : Fin n) ↦ MvPolynomial.X (i, false)))
    (∏ i : Fin n,
      ∏ i_1 ∈ Ioi i,
        (HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i_1, true)) (MvPolynomial.X (i, false)) -
          HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i, true)) (MvPolynomial.X (i_1, false))))
⊢ (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have hdet₁ : Eq.{u_1 + 1} (α := R)
  ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun (x : Fin n × Bool) ↦ (if x.2 = true then v else w) x.1 :
        (a : MvPolynomial (Fin n × Bool) ℤ) → R)
      (det (n := Fin n)
        (projVandermonde (fun (i : Fin n) ↦ MvPolynomial.X (i, true)) fun (i : Fin n) ↦ MvPolynomial.X (i, false))) :
    R)
  ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun (x : Fin n × Bool) ↦ (if x.2 = true then v else w) x.1 :
        (a : MvPolynomial (Fin n × Bool) ℤ) → R)
      (∏ i : Fin n,
        ∏ i_1 ∈ Ioi i,
          (HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i_1, true)) (MvPolynomial.X (i, false)) -
            HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i, true)) (MvPolynomial.X (i_1, false)))) :
    R)
Tactic: apply_fun MvPolynomial.eval₂Hom (Int.castRingHom R) (fun x ↦ (if x.2 then v else w) x.1) at hdet
Cleared hypotheses: hdet
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin n → R
u : (b : Bool) → (i : Fin n) → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun (b : Bool) (i : Fin n) ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ)) :
        (a : MvPolynomial (Fin n × Bool) ℤ) → FractionRing (MvPolynomial (Fin n × Bool) ℤ))
      (MvPolynomial.X (i, b))
hdet :
  Eq.{u_1 + 1} (α := R)
    ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun (x : Fin n × Bool) ↦ (if x.2 = true then v else w) x.1 :
          (a : MvPolynomial (Fin n × Bool) ℤ) → R)
        (det (n := Fin n)
          (projVandermonde (fun (i : Fin n) ↦ MvPolynomial.X (i, true)) fun (i : Fin n) ↦ MvPolynomial.X (i, false))) :
      R)
    ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun (x : Fin n × Bool) ↦ (if x.2 = true then v else w) x.1 :
          (a : MvPolynomial (Fin n × Bool) ℤ) → R)
        (∏ i : Fin n,
          ∏ i_1 ∈ Ioi i,
            (HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i_1, true)) (MvPolynomial.X (i, false)) -
              HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i, true))
                (MvPolynomial.X (i_1, false)))) :
      R)
⊢ (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have hdet₁ : Eq.{u_1 + 1} (α := R)
  (det (n := Fin n)
      ((RingHom.mapMatrix
            (MvPolynomial.eval₂Hom (Int.castRingHom R) fun (x : Fin n × Bool) ↦ (if x.2 = true then v else w) x.1) :
          (a : Matrix (Fin n) (Fin n) (MvPolynomial (Fin n × Bool) ℤ)) → Matrix (Fin n) (Fin n) R)
        (projVandermonde (fun (i : Fin n) ↦ MvPolynomial.X (i, true)) fun (i : Fin n) ↦ MvPolynomial.X (i, false))) :
    R)
  ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun (x : Fin n × Bool) ↦ (if x.2 = true then v else w) x.1 :
        (a : MvPolynomial (Fin n × Bool) ℤ) → R)
      (∏ i : Fin n,
        ∏ i_1 ∈ Ioi i,
          (HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i_1, true)) (MvPolynomial.X (i, false)) -
            HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i, true)) (MvPolynomial.X (i_1, false)))) :
    R)
Tactic: rw [RingHom.map_det] at hdet
Cleared hypotheses: hdet
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin n → R
u : (b : Bool) → (i : Fin n) → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun (b : Bool) (i : Fin n) ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ)) :
        (a : MvPolynomial (Fin n × Bool) ℤ) → FractionRing (MvPolynomial (Fin n × Bool) ℤ))
      (MvPolynomial.X (i, b))
hdet :
  Eq.{u_1 + 1} (α := R)
    (det (n := Fin n)
        ((RingHom.mapMatrix
              (MvPolynomial.eval₂Hom (Int.castRingHom R) fun (x : Fin n × Bool) ↦ (if x.2 = true then v else w) x.1) :
            (a : Matrix (Fin n) (Fin n) (MvPolynomial (Fin n × Bool) ℤ)) → Matrix (Fin n) (Fin n) R)
          (projVandermonde (fun (i : Fin n) ↦ MvPolynomial.X (i, true)) fun (i : Fin n) ↦ MvPolynomial.X (i, false))) :
      R)
    ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun (x : Fin n × Bool) ↦ (if x.2 = true then v else w) x.1 :
          (a : MvPolynomial (Fin n × Bool) ℤ) → R)
        (∏ i : Fin n,
          ∏ i_1 ∈ Ioi i,
            (HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i_1, true)) (MvPolynomial.X (i, false)) -
              HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i, true))
                (MvPolynomial.X (i_1, false)))) :
      R)
⊢ (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have h : projVandermonde v w =
  (RingHom.mapMatrix
        (MvPolynomial.eval₂Hom (Int.castRingHom R) fun (x : Fin n × Bool) ↦ (if x.2 = true then v else w) x.1) :
      (a : Matrix (Fin n) (Fin n) (MvPolynomial (Fin n × Bool) ℤ)) → Matrix (Fin n) (Fin n) R)
    (projVandermonde (fun (i : Fin n) ↦ MvPolynomial.X (i, true)) fun (i : Fin n) ↦ MvPolynomial.X (i, false))
Tactic: convert! hdet
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin n → R
u : (b : Bool) → (i : Fin n) → FractionRing (MvPolynomial (Fin n × Bool) ℤ) :=
  fun (b : Bool) (i : Fin n) ↦
    (algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ)) :
        (a : MvPolynomial (Fin n × Bool) ℤ) → FractionRing (MvPolynomial (Fin n × Bool) ℤ))
      (MvPolynomial.X (i, b))
hdet :
  Eq.{u_1 + 1} (α := R)
    (det (n := Fin n)
        ((RingHom.mapMatrix
              (MvPolynomial.eval₂Hom (Int.castRingHom R) fun (x : Fin n × Bool) ↦ (if x.2 = true then v else w) x.1) :
            (a : Matrix (Fin n) (Fin n) (MvPolynomial (Fin n × Bool) ℤ)) → Matrix (Fin n) (Fin n) R)
          (projVandermonde (fun (i : Fin n) ↦ MvPolynomial.X (i, true)) fun (i : Fin n) ↦ MvPolynomial.X (i, false))) :
      R)
    ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun (x : Fin n × Bool) ↦ (if x.2 = true then v else w) x.1 :
          (a : MvPolynomial (Fin n × Bool) ℤ) → R)
        (∏ i : Fin n,
          ∏ i_1 ∈ Ioi i,
            (HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i_1, true)) (MvPolynomial.X (i, false)) -
              HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i, true))
                (MvPolynomial.X (i_1, false)))) :
      R)
h :
  projVandermonde v w =
    (RingHom.mapMatrix
          (MvPolynomial.eval₂Hom (Int.castRingHom R) fun (x : Fin n × Bool) ↦ (if x.2 = true then v else w) x.1) :
        (a : Matrix (Fin n) (Fin n) (MvPolynomial (Fin n × Bool) ℤ)) → Matrix (Fin n) (Fin n) R)
      (projVandermonde (fun (i : Fin n) ↦ MvPolynomial.X (i, true)) fun (i : Fin n) ↦ MvPolynomial.X (i, false))
⊢ (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have h₁ : Eq.{u_1 + 1} (α := R) (∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j) : R)
  ((MvPolynomial.eval₂Hom (Int.castRingHom R) fun (x : Fin n × Bool) ↦ (if x.2 = true then v else w) x.1 :
        (a : MvPolynomial (Fin n × Bool) ℤ) → R)
      (∏ i : Fin n,
        ∏ i_1 ∈ Ioi i,
          (HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i_1, true)) (MvPolynomial.X (i, false)) -
            HMul.hMul (α := MvPolynomial (Fin n × Bool) ℤ) (MvPolynomial.X (i, true)) (MvPolynomial.X (i_1, false)))) :
    R)
Tactic: convert! hdet
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
v : Fin n → R
⊢ (vandermonde v).det = 0 ↔ ∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j
have mp : (vandermonde v).det = 0 → ∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
v : Fin n → R
mp : (vandermonde v).det = 0 → ∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j
⊢ (vandermonde v).det = 0 ↔ ∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j
have mpr : (∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j) → (vandermonde v).det = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
v : Fin n → R
⊢ (vandermonde v).det = 0 → ∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j
have mp : ∀ (x : Fin n) (h : Membership.mem (γ := Finset (Fin n)) univ x ∧ ∃ a ∈ Ioi x, v a = v x),
  ∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j
Tactic: simp only [det_vandermonde v, Finset.prod_eq_zero_iff, sub_eq_zero, forall_exists_index]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
v : Fin n → R
⊢ (∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j) → (vandermonde v).det = 0
have mpr : ∀ (x x_1 : Fin n), v x = v x_1 → ¬x = x_1 → (vandermonde v).det = 0
Tactic: simp only [Ne, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
v : Fin n → R
⊢ ∀ (x x_1 : Fin n), v x = v x_1 → ¬x = x_1 → (vandermonde v).det = 0
have mpr : ∀ (i j : Fin n) (h₁ : v i = v j) (h₂ : ¬i = j) (k : Fin n), vandermonde v i k = vandermonde v j k
Tactic: refine fun i j h₁ h₂ => Matrix.det_zero_of_row_eq h₂ (funext fun k => ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
v : Fin n → R
i j : Fin n
h₁ : v i = v j
h₂ : ¬i = j
k : Fin n
⊢ vandermonde v i k = vandermonde v j k
have mpr : v i ^ (↑k : ℕ) = vandermonde v j k
Tactic: rw [vandermonde_apply, vandermonde_apply, h₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
v : Fin n → R
i j : Fin n
h₁ : v i = v j
h₂ : ¬i = j
k : Fin n
mpr : v i ^ (↑k : ℕ) = vandermonde v j k
⊢ vandermonde v i k = vandermonde v j k
have mpr₁ : v i ^ (↑k : ℕ) = v j ^ (↑k : ℕ)
Tactic: rw [vandermonde_apply, vandermonde_apply, h₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
v : Fin n → R
i j : Fin n
h₁ : v i = v j
h₂ : ¬i = j
k : Fin n
mpr : v i ^ (↑k : ℕ) = vandermonde v j k
mpr₁ : v i ^ (↑k : ℕ) = v j ^ (↑k : ℕ)
⊢ vandermonde v i k = vandermonde v j k
have mpr₂ : v j ^ (↑k : ℕ) = v j ^ (↑k : ℕ)
Tactic: rw [vandermonde_apply, vandermonde_apply, h₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
a : R
⊢ det (n := Fin n) (vandermonde fun (i : Fin n) ↦ v i - a) = (vandermonde v).det
have 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))
Tactic: rw [← det_vandermonde_add v (-a)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
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
⊢ v = 0
have apply : ∀ (j : Fin n), Eq.{u_1 + 1} (α := R) (∑ i : Fin n, f j ^ (↑i : ℕ) * v i) 0
Tactic: apply eq_zero_of_forall_index_sum_pow_mul_eq_zero hf