Complex.Hadamard.exists_ball_divisorComplementCanonicalProduct_ne_zero

theorem exists_ball_divisorComplementCanonicalProduct_ne_zero    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) :    ∃ r > 0, ∀ z ∈ Metric.ball z₀ r, divisorComplementCanonicalProduct m f z₀ z ≠ 0 := by  have hdiff :      DifferentiableOn ℂ (divisorComplementCanonicalProduct m f z₀) (Set.univ : Set ℂ) :=    differentiableOn_divisorComplementCanonicalProduct_univ (m := m) (f := f) (z₀ := z₀) h_sum  have hdiffAt : DifferentiableAt ℂ (divisorComplementCanonicalProduct m f z₀) z₀ := by    exact (hdiff z₀ (by simp)).differentiableAt (by simp)  have hcont : ContinuousAt (divisorComplementCanonicalProduct m f z₀) z₀ :=    hdiffAt.continuousAt  have h0 : divisorComplementCanonicalProduct m f z₀ z₀ ≠ 0 :=    divisorComplementCanonicalProduct_ne_zero_at (m := m) (f := f) (z₀ := z₀) h_sum  have hopen : IsOpen (({0} : Set ℂ)ᶜ) := isClosed_singleton.isOpen_compl  have hmem : divisorComplementCanonicalProduct m f z₀ z₀ ∈ (({0} : Set ℂ)ᶜ) := by    simp [h0]  rcases (Metric.mem_nhds_iff.1 (hcont (hopen.mem_nhds hmem))) with ⟨r, hrpos, hr⟩  refine ⟨r, hrpos, ?_⟩  intro z hz  have : divisorComplementCanonicalProduct m f z₀ z ∈ ({0} : Set ℂ)ᶜ := hr hz  simpa using this