Bennett Local Residue eq decomposition coeff

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.Polynomial.BigOperators
import Mathlib.Algebra.Polynomial.PartialFractions
import Mathlib.Algebra.Polynomial.RingDivision
import Mathlib.RingTheory.PowerSeries.Binomial
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_BennettLocalResidues_Definitions
import Definitions.Def_D1Bound5_BennettResidueCoefficient_Definitions

section
open Finset

namespace D1Bound5

section Field

variable {F ι : Type*} [Field F] [CharZero F]
variable [Fintype ι] [DecidableEq ι]




















theorem _root_.D1Bound5.bennettLocalResidue_eq_decomposition_coeff
    (a : ι → F) (ha : Function.Injective a) (e : ι → ℕ)
    (c : (l : ι) → Fin (e l + 1) → F) (f : Polynomial F)
    (hc : f = ∑ l, ∑ j : Fin (e l + 1),
      Polynomial.C (c l j) * clearedPoleNumerator a e l j) (i : ι) :
    bennettLocalResidue a e f i = c i (Fin.last (e i)) := by sorry



end Field

end D1Bound5
end