Complex.Hadamard.differentiableOn_update_limUnder_divisorCanonicalProduct_div_pow

theorem differentiableOn_update_limUnder_divisorCanonicalProduct_div_pow    (m : ℕ) (f : ℂ → ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))    (z₀ : ℂ) : ∃ r > 0, DifferentiableOn ℂ (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)))        (Metric.ball z₀ r) := by  rcases bddAbove_norm_divisorCanonicalProduct_div_pow_puncturedBall (m := m) (f := f)      (h_sum := h_sum) (z₀ := z₀) with ⟨r, hrpos, hbdd⟩  refine ⟨r, hrpos, ?_⟩  have hnhds : Metric.ball z₀ r ∈ 𝓝 z₀ := Metric.ball_mem_nhds z₀ hrpos  have hdiff : DifferentiableOn ℂ (fun z : ℂ =>        (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) /          (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card)      ((Metric.ball z₀ r) \ {z₀}) := by    have hglob :=      differentiableOn_divisorCanonicalProduct_div_pow_sub        (m := m) (f := f) h_sum (z₀ := z₀)        (k := (divisorZeroIndex₀_fiberFinset (f := f) z₀).card)    refine hglob.mono ?_    intro z hz    exact ⟨by simp, hz.2⟩  have hb : BddAbove (norm ∘ (fun z : ℂ => (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) /      (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card) ''    ((Metric.ball z₀ r) \ {z₀})) := hbdd  simpa using    (Complex.differentiableOn_update_limUnder_of_bddAbove (f := fun z : ℂ =>        (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) /          (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card)      (s := Metric.ball z₀ r) (c := z₀) hnhds hdiff hb)