Complex.Hadamard.tendstoUniformlyOn_divisorPartialProduct_div_pow_sub

theorem tendstoUniformlyOn_divisorPartialProduct_div_pow_sub    (m : ℕ) (f : ℂ → ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))    (z₀ : ℂ) (k : ℕ) {K : Set ℂ} (hK : IsCompact K) (hKz : ∀ z ∈ K, z ≠ z₀) :    TendstoUniformlyOn      (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 ℂ))))      K := by  have hloc :      TendstoLocallyUniformlyOn        (fun s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) => divisorPartialProduct m f s)        (divisorCanonicalProduct m f (Set.univ : Set ℂ))        Filter.atTop        K :=    (tendstoLocallyUniformlyOn_divisorPartialProduct_univ (m := m) (f := f) h_sum).mono      (by intro z hz; simp)  have hunif :      TendstoUniformlyOn        (fun s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) => divisorPartialProduct m f s)        (divisorCanonicalProduct m f (Set.univ : Set ℂ))        Filter.atTop        K :=    (tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK).1 hloc  let h : ℂ → ℂ := fun z => ((z - z₀) ^ k)⁻¹  have hh : ∃ C, ∀ z ∈ K, ‖h z‖ ≤ C := by    have hcont : ContinuousOn h K := by      have hpow : ContinuousOn (fun z : ℂ => (z - z₀) ^ k) K := by        fun_prop      refine hpow.inv₀ ?_      intro z hz      have hz0 : z - z₀ ≠ 0 := sub_ne_zero.mpr (hKz z hz)      exact pow_ne_zero k hz0    have hKimg : IsCompact (h '' K) := hK.image_of_continuousOn hcont    rcases (isBounded_iff_forall_norm_le.1 hKimg.isBounded) with ⟨C, hC⟩    refine ⟨C, ?_⟩    intro z hz    exact hC (h z) ⟨z, hz, rfl⟩  have hunif' :=    (TendstoUniformlyOn.mul_left_bounded (p := (Filter.atTop : Filter (Finset (divisorZeroIndex₀ f    (Set.univ : Set ℂ)))))        (K := K)        (F := fun s z => divisorPartialProduct m f s z)        (f := fun z => divisorCanonicalProduct m f (Set.univ : Set ℂ) z)        (h := h)        hunif hh)  simpa [h, div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] using hunif'