Complex.Hadamard.exists_entire_nonzero_hadamardQuotient

theorem exists_entire_nonzero_hadamardQuotient    (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))) :    ∃ H : ℂ → ℂ, Differentiable ℂ H ∧ (∀ z, H z ≠ 0) ∧ ∀ z : ℂ, f z =      H z * z ^ (analyticOrderNatAt f 0) * divisorCanonicalProduct m f (Set.univ : Set ℂ) z := by  let denom : ℂ → ℂ := hadamardDenom m f  let q : ℂ → ℂ := fun z => f z / denom z  have hden_entire : Differentiable ℂ denom :=    differentiable_hadamardDenom (m := m) f h_sum  have hq_mero : MeromorphicOn q (Set.univ : Set ℂ) := by    intro z hzU    have hf_m : MeromorphicAt f z := (hf.analyticAt z).meromorphicAt    have hden_m : MeromorphicAt denom z := (hden_entire.analyticAt z).meromorphicAt    simpa [q, denom, div_eq_mul_inv] using! (hf_m.mul hden_m.inv)  let H : ℂ → ℂ := toMeromorphicNFOn q (Set.univ : Set ℂ)  have hNF : MeromorphicNFOn H (Set.univ : Set ℂ) :=    meromorphicNFOn_toMeromorphicNFOn q (Set.univ : Set ℂ)  have hdivH : MeromorphicOn.divisor H (Set.univ : Set ℂ) = 0 := by    have hdivq : MeromorphicOn.divisor q (Set.univ : Set ℂ) = 0 :=      divisor_hadamardQuotient_eq_zero (m := m) (f := f) (hf := hf)        (hnot := hnot) (h_sum := h_sum)    simpa [H, hdivq] using      (MeromorphicOn.divisor_of_toMeromorphicNFOn        (f := q) (U := (Set.univ : Set ℂ)) hq_mero)  have hA : AnalyticOnNhd ℂ H (Set.univ : Set ℂ) := by    have :        (0 : Function.locallyFinsuppWithin (Set.univ : Set ℂ) ℤ) ≤          MeromorphicOn.divisor H (Set.univ : Set ℂ) := by      simp [hdivH]    exact (MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd (h₁f := hNF)).1 (by simp [hdivH])  have hH_entire : Differentiable ℂ H := by    intro z    exact (hA z (by simp)).differentiableAt  rcases hnot with ⟨z1, hz1⟩  have hden1 : denom z1 ≠ 0 :=    hadamardDenom_ne_zero_at (m := m) (f := f) hf ⟨z1, hz1⟩ h_sum hz1  have hqA1 : AnalyticAt ℂ q z1 := by    have hdenA1 : AnalyticAt ℂ denom z1 := hden_entire.analyticAt z1    exact (hf.analyticAt z1).div hdenA1 hden1  have hqNF1 : MeromorphicNFAt q z1 := hqA1.meromorphicNFAt  have htoEq : toMeromorphicNFAt q z1 = q := (toMeromorphicNFAt_eq_self (f := q) (x := z1)).2 hqNF1  have hH1 : H z1 = q z1 := by    have hx : z1 ∈ (Set.univ : Set ℂ) := by simp    have : toMeromorphicNFOn q (Set.univ : Set ℂ) z1 = toMeromorphicNFAt q z1 z1 :=      (toMeromorphicNFOn_eq_toMeromorphicNFAt (f := q) (U := (Set.univ : Set ℂ)) hq_mero hx)    simpa [H, htoEq] using this  have hH1_ne : H z1 ≠ 0 := by    have : q z1 ≠ 0 := div_ne_zero hz1 hden1    simpa [hH1] using this  have hH_not_top : ∀ z : ℂ, analyticOrderAt H z ≠ ⊤ := by    exact analyticOrderAt_ne_top_of_exists_ne_zero (hf := hH_entire) ⟨z1, hH1_ne⟩  have hH_orderNat_zero : ∀ z : ℂ, analyticOrderNatAt H z = 0 := by    intro z    have hzdiv :        (MeromorphicOn.divisor H (Set.univ : Set ℂ)) z = (analyticOrderNatAt H z : ℤ) := by      simpa using (divisor_univ_eq_analyticOrderNatAt_int (f := H) hH_entire z)    have : (MeromorphicOn.divisor H (Set.univ : Set ℂ)) z = 0 := by      simp [hdivH]    have : (analyticOrderNatAt H z : ℤ) = 0 := by simpa [hzdiv] using this    exact_mod_cast this  have hH_ne : ∀ z : ℂ, H z ≠ 0 := by    intro z    have hcast : (analyticOrderNatAt H z : ℕ∞) = analyticOrderAt H z :=      Nat.cast_analyticOrderNatAt (f := H) (z₀ := z) (hH_not_top z)    have : analyticOrderAt H z = 0 := by      have : (analyticOrderNatAt H z : ℕ∞) = 0 := by exact_mod_cast (hH_orderNat_zero z)      simpa [hcast] using this    exact ((hA z (by simp)).analyticOrderAt_eq_zero).1 this  have hfA : AnalyticOnNhd ℂ f (Set.univ : Set ℂ) := fun z hzU => hf.analyticAt z  have hdenA : AnalyticOnNhd ℂ denom (Set.univ : Set ℂ) := fun z hzU => hden_entire.analyticAt z  have hprodA : AnalyticOnNhd ℂ (fun z => H z * denom z) (Set.univ : Set ℂ) :=    (hA.mul hdenA)  have hlocal : f =ᶠ[𝓝 z1] fun z => H z * denom z := by    have hden_ne : ∀ᶠ z in 𝓝 z1, denom z ≠ 0 :=      (hden_entire.differentiableAt.continuousAt.ne_iff_eventually_ne continuousAt_const).1 hden1    have hH_eq_q : H =ᶠ[𝓝 z1] q := by      have hx : z1 ∈ (Set.univ : Set ℂ) := by simp      have hloc :          toMeromorphicNFOn q (Set.univ : Set ℂ) =ᶠ[𝓝 z1] toMeromorphicNFAt q z1 := by        simpa [H] using (toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds (f := q)          (U := (Set.univ : Set ℂ)) hq_mero hx)      simpa [H, htoEq] using hloc    filter_upwards [hden_ne, hH_eq_q] with z hzden hHz    have hcancel : q z * denom z = f z := by      dsimp [q]      field_simp [hzden]    calc      f z = q z * denom z := hcancel.symm      _ = H z * denom z := by simp [hHz]  have hglob : f = fun z => H z * denom z :=    AnalyticOnNhd.eq_of_eventuallyEq (hf := hfA) (hg := hprodA) hlocal  refine ⟨H, hH_entire, hH_ne, ?_⟩  intro z  have hglobz : f z = H z * denom z := congrArg (fun g => g z) hglob  simpa [denom, hadamardDenom, mul_assoc, mul_left_comm, mul_comm] using hglobz