Complex.Hadamard.analyticAt_update_limUnder_divisorCanonicalProduct_div_pow

theorem analyticAt_update_limUnder_divisorCanonicalProduct_div_pow    (m : ℕ) (f : ℂ → ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))    (z₀ : ℂ) : AnalyticAt ℂ (Function.update (fun z : ℂ =>          (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) /        (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card) z₀        (limUnder (𝓝[≠] z₀) (fun z : ℂ => (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) /              (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card)))      z₀ := by  rcases      differentiableOn_update_limUnder_divisorCanonicalProduct_div_pow        (m := m) (f := f) h_sum (z₀ := z₀) with ⟨r, hrpos, hdiff⟩  let g : ℂ → ℂ :=    Function.update      (fun z : ℂ =>        (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) /          (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card)      z₀      (limUnder (𝓝[≠] z₀) fun z : ℂ =>        (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) /          (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card)  have hcont : ContinuousAt g z₀ :=    (hdiff.differentiableAt (Metric.ball_mem_nhds z₀ hrpos)).continuousAt  have hd :      ∀ᶠ z in 𝓝[≠] z₀, DifferentiableAt ℂ g z := by    have hballWithin : Metric.ball z₀ r ∈ 𝓝[≠] z₀ := by      refine mem_nhdsWithin_iff_exists_mem_nhds_inter.2 ?_      refine ⟨Metric.ball z₀ r, Metric.ball_mem_nhds z₀ hrpos, ?_⟩      intro z hz      exact hz.1    filter_upwards [hballWithin] with z hz    exact (hdiff z hz).differentiableAt (Metric.isOpen_ball.mem_nhds hz)  simpa [g] using Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt hd hcont