Coherent Weights3 eq quotient

import Mathlib.Algebra.BigOperators.NatAntidiagonal
import Mathlib.Analysis.Analytic.Binomial
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Normed.Ring.Basic
import Mathlib.Analysis.SpecificLimits.Normed
import Mathlib.Data.Fin.VecNotation
import Mathlib.Data.Finset.Insert
import Mathlib.Data.Sym.Basic
import Mathlib.Data.Sym.Card
import Mathlib.LinearAlgebra.Lagrange
import Mathlib.RingTheory.Binomial
import Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
import Definitions.Def_D1Bound5_CoherentPolynomialWeights_Definitions

section
open Finset

namespace D1Bound5















theorem _root_.D1Bound5.coherentWeights3_eq_quotient
    {F : Type*} [Field F] (a : Fin 3 → F) (hinj : Function.Injective a)
    (i : Fin 3) :
    coherentWeights3 a i = coherentVandermonde3 a * (a i) ^ (3 - 2) /
      (∏ j ∈ Finset.univ.erase i, (a i - a j)) := by sorry















end D1Bound5
end