Complex.Hadamard.eventually_eq_punctured_quotient_of_factorization

theorem eventually_eq_punctured_quotient_of_factorization    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ) :    ∀ᶠ s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) in (Filter.atTop : Filter _),      ∃ g : ℂ → ℂ, AnalyticAt ℂ g z₀ ∧ (fun z : ℂ => (divisorPartialProduct m f s z) /            (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card)            =ᶠ[𝓝[≠] z₀] g := by  refine (eventually_exists_analyticAt_eq_pow_smul_divisorPartialProduct (m := m)    (f := f) z₀).mono ?_  intro s hs  rcases hs with ⟨g, hg, hg0, hEq⟩  refine ⟨g, hg, ?_⟩  have hEq' : (fun z : ℂ => divisorPartialProduct m f s z) =ᶠ[𝓝[≠] z₀]        fun z : ℂ => (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card • g z :=    hEq.filter_mono nhdsWithin_le_nhds  have hne : ∀ᶠ z : ℂ in 𝓝[≠] z₀, z ≠ z₀ := by    simpa [Filter.Eventually] using! (self_mem_nhdsWithin : {z : ℂ | z ≠ z₀} ∈ 𝓝[≠] z₀)  filter_upwards [hEq', hne] with z hz hzne  have hz0 : (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card ≠ 0 :=    pow_ne_zero _ (sub_ne_zero.mpr hzne)  have : (divisorPartialProduct m f s z) / (z - z₀) ^ (divisorZeroIndex₀_fiberFinset      (f := f) z₀).card = g z := by    rw [hz]    simpa [smul_eq_mul] using (mul_div_cancel_left₀ (g z) hz0)  simpa [divisorPartialProduct] using this