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

Tactic:
norm_cast at hdet