Complex.Hadamard.tendstoLocallyUniformlyOn_divisorPartialProduct_div_pow_sub

theorem tendstoLocallyUniformlyOn_divisorPartialProduct_div_pow_sub    (m : ℕ) (f : ℂ → ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))    (z₀ : ℂ) (k : ℕ) :    TendstoLocallyUniformlyOn      (fun s z => (divisorPartialProduct m f s z) / (z - z₀) ^ k)      (fun z => (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) / (z - z₀) ^ k)      (Filter.atTop : Filter (Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ))))      ((Set.univ : Set ℂ) \ {z₀}) := by  have hopen : IsOpen ((Set.univ : Set ℂ) \ {z₀}) := by    have hset : ((Set.univ : Set ℂ) \ {z₀}) = ({z₀} : Set ℂ)ᶜ := by      ext z      simp    simp [hset]  refine (tendstoLocallyUniformlyOn_iff_forall_isCompact hopen).2 ?_  intro K hKsub hK  have hKz : ∀ z ∈ K, z ≠ z₀ := by    intro z hzK    have : z ∈ (Set.univ : Set ℂ) \ {z₀} := hKsub hzK    exact by simpa [Set.mem_sdiff, Set.mem_singleton_iff] using this.2  exact tendstoUniformlyOn_divisorPartialProduct_div_pow_sub    (m := m) (f := f) h_sum (z₀ := z₀) (k := k) (hK := hK) hKz