Bennett Cleared Taylor eval remove pole

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.Polynomial.BigOperators
import Mathlib.Algebra.Polynomial.Degree.Operations
import Mathlib.RingTheory.PowerSeries.Binomial
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_BennettClearedResidues_Definitions
import Definitions.Def_D1Bound5_BennettPoleSeries_Definitions

section
open Finset

namespace D1Bound5

variable {F : Type*} [Field F] [CharZero F]








theorem _root_.D1Bound5.bennettClearedTaylor_eval_remove_pole
    (k r : ℕ) (hr : r ≤ k) (ν a N : F) (B : PowerSeries F)
    (hd : N + a ≠ 0) :
    (bennettClearedTaylor k r ν a
      (bennettPoleSeries (N + a) k * B)).eval N =
      ((N + a)⁻¹) ^ k *
        (bennettClearedTaylor k r (ν - (k : F)) a B).eval N := by sorry

section Nodes

variable {I : Type*} [DecidableEq I]

















end Nodes

end D1Bound5
end