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
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
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
⊢ W 0 j.succ = 0

Tactic:
simp only [of_apply, projVandermonde_apply_of_ne_zero h0, val_succ, val_castSucc, cons_succ, W, r]

Premises used: Fin.cons_succ, Matrix.projVandermonde_apply_of_ne_zero, Fin.val_succ, Matrix.of_apply, 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
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
⊢ 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:
ring
-- Module: Mathlib.LinearAlgebra.Vandermonde
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 (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)
-- Module: Mathlib.LinearAlgebra.Vandermonde
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 :
  (projVandermonde (u true) (u false)).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (u true j * u false i - u true i * u false j)
⊢ 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))))
    (∏ x : Fin n,
      ∏ x_1 ∈ Ioi x,
        (HMul.hMul (α := FractionRing (MvPolynomial (Fin n × Bool) ℤ)) (β :=
            FractionRing (MvPolynomial (Fin n × Bool) ℤ))
            ((algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ)) :
                  (a : MvPolynomial (Fin n × Bool) ℤ) → FractionRing (MvPolynomial (Fin n × Bool) ℤ))
                (MvPolynomial.X (x_1, true)) :
              FractionRing (MvPolynomial (Fin n × Bool) ℤ))
            ((algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ)) :
                  (a : MvPolynomial (Fin n × Bool) ℤ) → FractionRing (MvPolynomial (Fin n × Bool) ℤ))
                (MvPolynomial.X (x, false)) :
              FractionRing (MvPolynomial (Fin n × Bool) ℤ)) -
          HMul.hMul (α := FractionRing (MvPolynomial (Fin n × Bool) ℤ)) (β :=
            FractionRing (MvPolynomial (Fin n × Bool) ℤ))
            ((algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ)) :
                  (a : MvPolynomial (Fin n × Bool) ℤ) → FractionRing (MvPolynomial (Fin n × Bool) ℤ))
                (MvPolynomial.X (x, true)) :
              FractionRing (MvPolynomial (Fin n × Bool) ℤ))
            ((algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ)) :
                  (a : MvPolynomial (Fin n × Bool) ℤ) → FractionRing (MvPolynomial (Fin n × Bool) ℤ))
                (MvPolynomial.X (x_1, false)) :
              FractionRing (MvPolynomial (Fin n × Bool) ℤ))))

Tactic:
simp only [u] at hdet
-- Module: Mathlib.LinearAlgebra.Vandermonde
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) ℤ))
⊢ 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

Premises used: IsFractionRing.coe_inj, Matrix.projVandermonde_map, RingHom.map_det
-- Module: Mathlib.LinearAlgebra.Vandermonde
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))))
⊢ 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

Premises used: MvPolynomial.eval₂Hom, Int.castRingHom
-- Module: Mathlib.LinearAlgebra.Vandermonde
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)
⊢ 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

Premises used: RingHom.map_det
-- Module: Mathlib.LinearAlgebra.Vandermonde
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)
⊢ 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:
hdet
-- Module: Mathlib.LinearAlgebra.Vandermonde
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))
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)
⊢ (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)

Tactic:
convert! hdet
-- Module: Mathlib.LinearAlgebra.Vandermonde
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 =
    (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:
simp [← Matrix.ext_iff, projVandermonde_apply]

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

Premises used: Matrix.ext_iff, Matrix.projVandermonde_apply
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
⊢ (vandermonde v).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)

Tactic:
simp [vandermonde_eq_projVandermonde, det_projVandermonde]

Premises used: Matrix.det_projVandermonde, Matrix.vandermonde_eq_projVandermonde
-- Module: Mathlib.LinearAlgebra.Vandermonde
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
mpr : (∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j) → (vandermonde v).det = 0
⊢ (vandermonde v).det = 0 ↔ ∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
v : Fin n → R
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
⊢ (vandermonde v).det = 0 → ∃ (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]

Premises used: Matrix.det_vandermonde, sub_eq_zero, forall_exists_index, Finset.prod_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
v : Fin n → R
i : Fin n
left : Membership.mem (γ := Finset (Fin n)) univ i
j : Fin n
h₁ : j ∈ Ioi i
h₂ : v j = v i
⊢ ∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j

Tactic:
⟨j, i, h₂, (mem_Ioi.mp h₁).ne'⟩

Premises used: Finset.mem_Ioi, LT.lt.ne', And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
v : Fin n → R
i : Fin n
left : Membership.mem (γ := Finset (Fin n)) univ i
j : Fin n
h₁ : j ∈ Ioi i
h₂ : v j = v i
⊢ ∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j

Tactic:
exact ⟨j, i, h₂, (mem_Ioi.mp h₁).ne'⟩
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
v : Fin n → R
mpr : ∀ (x x_1 : Fin n), v x = v x_1 → ¬x = x_1 → (vandermonde v).det = 0
⊢ (∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j) → (vandermonde v).det = 0

Tactic:
simp only [Ne, forall_exists_index, and_imp]

Premises used: and_imp, forall_exists_index, Ne
-- Module: Mathlib.LinearAlgebra.Vandermonde
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

Tactic:
fun i j h₁ h₂ => Matrix.det_zero_of_row_eq h₂ (funext fun k => ?_)

Premises used: Matrix.det_zero_of_row_eq, funext
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
v : Fin n → R
mpr : ∀ (i j : Fin n) (h₁ : v i = v j) (h₂ : ¬i = j) (k : Fin n), vandermonde v i k = vandermonde v j k
⊢ ∀ (x x_1 : Fin n), v x = v x_1 → ¬x = x_1 → (vandermonde v).det = 0

Tactic:
refine fun i j h₁ h₂ => Matrix.det_zero_of_row_eq h₂ (funext fun k => ?_)

Premises used: Matrix.det_zero_of_row_eq, funext
-- Module: Mathlib.LinearAlgebra.Vandermonde
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 : ℕ)
mpr₂ mpr₃ : v j ^ (↑k : ℕ) = v j ^ (↑k : ℕ)
⊢ vandermonde v i k = vandermonde v j k

Tactic:
rw [vandermonde_apply, vandermonde_apply, h₁]

Premises used: Matrix.vandermonde_apply
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : IsDomain R
v : Fin n → R
⊢ (vandermonde v).det ≠ 0 ↔ ∀ ⦃a₁ a₂ : Fin n⦄, v a₁ = v a₂ → a₁ = a₂

Tactic:
simp only [det_vandermonde_eq_zero_iff, Ne, not_exists, not_and, Classical.not_not]

Premises used: Classical.not_not, not_exists, Ne, Matrix.det_vandermonde_eq_zero_iff, not_and
-- Module: Mathlib.LinearAlgebra.Vandermonde
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

Tactic:
simp [Matrix.det_vandermonde]

Premises used: Matrix.det_vandermonde