-- 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))))
    (∏ 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) ℤ))))
⊢ (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
have 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) ℤ))
Tactic: norm_cast at hdet
Cleared hypotheses: hdet