Complex.Hadamard.divisor_hadamardQuotient_eq_zero

theorem divisor_hadamardQuotient_eq_zero    (m : ℕ) {f : ℂ → ℂ} (hf : Differentiable ℂ f) (hnot : ∃ z : ℂ, f z ≠ 0)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) :    MeromorphicOn.divisor (fun z : ℂ => f z / hadamardDenom m f z) (Set.univ : Set ℂ) = 0 := by  have hf_mero : MeromorphicOn f (Set.univ : Set ℂ) := by    intro z hz    exact (hf.analyticAt z).meromorphicAt  have hden_entire : Differentiable ℂ (hadamardDenom m f) :=    differentiable_hadamardDenom (m := m) f h_sum  have hden_mero : MeromorphicOn (hadamardDenom m f) (Set.univ : Set ℂ) := by    intro z hz    exact (hden_entire.analyticAt z).meromorphicAt  rcases hnot with ⟨z1, hz1⟩  have hden1 : hadamardDenom m f z1 ≠ 0 :=    hadamardDenom_ne_zero_at (m := m) (f := f) hf ⟨z1, hz1⟩ h_sum hz1  have hf_order_ne_top : ∀ z ∈ (Set.univ : Set ℂ), meromorphicOrderAt f z ≠ ⊤ := by    intro z hzU    have hz1_ne_top : meromorphicOrderAt f z1 ≠ ⊤ := by      have hfAt : MeromorphicAt f z1 := hf_mero z1 (by simp)      have hcont : ContinuousAt f z1 := (hf.differentiableAt).continuousAt      have hne_nhds : ∀ᶠ w in 𝓝 z1, f w ≠ 0 :=        (hcont.ne_iff_eventually_ne continuousAt_const).1 hz1      have hne_nhdsNE : ∀ᶠ w in 𝓝[≠] z1, f w ≠ 0 :=        eventually_nhdsWithin_of_eventually_nhds hne_nhds      exact (meromorphicOrderAt_ne_top_iff_eventually_ne_zero (hf := hfAt)).2 hne_nhdsNE    exact MeromorphicOn.meromorphicOrderAt_ne_top_of_isPreconnected (hf := hf_mero)      (x := z1) (hU := isPreconnected_univ) (h₁x := by simp) (hy := by simp) hz1_ne_top  have hden_order_ne_top :      ∀ z ∈ (Set.univ : Set ℂ), meromorphicOrderAt (hadamardDenom m f) z ≠ ⊤ := by    intro z hzU    have hz1_ne_top : meromorphicOrderAt (hadamardDenom m f) z1 ≠ ⊤ := by      have hdenAt : MeromorphicAt (hadamardDenom m f) z1 := hden_mero z1 (by simp)      have hcont : ContinuousAt (hadamardDenom m f) z1 :=        (hden_entire.differentiableAt).continuousAt      have hne_nhds : ∀ᶠ w in 𝓝 z1, hadamardDenom m f w ≠ 0 :=        (hcont.ne_iff_eventually_ne continuousAt_const).1 hden1      have hne_nhdsNE : ∀ᶠ w in 𝓝[≠] z1, hadamardDenom m f w ≠ 0 :=        eventually_nhdsWithin_of_eventually_nhds hne_nhds      exact (meromorphicOrderAt_ne_top_iff_eventually_ne_zero (hf := hdenAt)).2 hne_nhdsNE    exact MeromorphicOn.meromorphicOrderAt_ne_top_of_isPreconnected (hf := hden_mero)      (x := z1) (hU := isPreconnected_univ) (h₁x := by simp) (hy := by simp) hz1_ne_top  have hinv_order_ne_top :      ∀ z ∈ (Set.univ : Set ℂ),        meromorphicOrderAt (fun z : ℂ => (hadamardDenom m f z)⁻¹) z ≠ ⊤ := by    intro z hzU    have hinv_mero :        MeromorphicOn (fun z : ℂ => (hadamardDenom m f z)⁻¹) (Set.univ : Set ℂ) :=      hden_mero.inv    have hz1_ne_top :        meromorphicOrderAt (fun z : ℂ => (hadamardDenom m f z)⁻¹) z1 ≠ ⊤ := by      have hinvAt : MeromorphicAt (fun z : ℂ => (hadamardDenom m f z)⁻¹) z1 :=        hinv_mero z1 (by simp)      have hcont_denom : ContinuousAt (hadamardDenom m f) z1 :=        (hden_entire.differentiableAt).continuousAt      have hcont : ContinuousAt (fun z : ℂ => (hadamardDenom m f z)⁻¹) z1 :=        hcont_denom.inv₀ hden1      have hinv1 : (fun z : ℂ => (hadamardDenom m f z)⁻¹) z1 ≠ 0 := by        simpa using inv_ne_zero hden1      have hne_nhds :          ∀ᶠ w in 𝓝 z1, (fun z : ℂ => (hadamardDenom m f z)⁻¹) w ≠ 0 :=        (hcont.ne_iff_eventually_ne continuousAt_const).1 hinv1      have hne_nhdsNE :          ∀ᶠ w in 𝓝[≠] z1, (fun z : ℂ => (hadamardDenom m f z)⁻¹) w ≠ 0 :=        eventually_nhdsWithin_of_eventually_nhds hne_nhds      exact (meromorphicOrderAt_ne_top_iff_eventually_ne_zero (hf := hinvAt)).2 hne_nhdsNE    exact MeromorphicOn.meromorphicOrderAt_ne_top_of_isPreconnected (hf := hinv_mero)      (x := z1) (hU := isPreconnected_univ) (h₁x := by simp) (hy := by simp) hz1_ne_top  have hdiv_denom : MeromorphicOn.divisor (hadamardDenom m f) (Set.univ : Set ℂ) =      MeromorphicOn.divisor f (Set.univ : Set ℂ) :=    divisor_hadamardDenom_eq (m := m) (hf := hf) (h_sum := h_sum)  calc    MeromorphicOn.divisor (fun z : ℂ => f z / hadamardDenom m f z) (Set.univ : Set ℂ)        = MeromorphicOn.divisor            (fun z : ℂ => f z * (hadamardDenom m f z)⁻¹) (Set.univ : Set ℂ) := by            simp [div_eq_mul_inv]    _ = MeromorphicOn.divisor f (Set.univ : Set ℂ) +          MeromorphicOn.divisor (fun z : ℂ => (hadamardDenom m f z)⁻¹) (Set.univ : Set ℂ) := by          simpa using (MeromorphicOn.divisor_fun_mul (U := (Set.univ : Set ℂ))            (f₁ := f) (f₂ := fun z => (hadamardDenom m f z)⁻¹) hf_mero (hden_mero.inv)            hf_order_ne_top hinv_order_ne_top)    _ = MeromorphicOn.divisor f (Set.univ : Set ℂ) -          MeromorphicOn.divisor (hadamardDenom m f) (Set.univ : Set ℂ) := by          simp [sub_eq_add_neg]    _ = 0 := by          simp [hdiv_denom]