Complex.Hadamard.differentiableOn_divisorCanonicalProduct_univ

theorem differentiableOn_divisorCanonicalProduct_univ    (m : ℕ) (f : ℂ → ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) :    DifferentiableOn ℂ (divisorCanonicalProduct m f (Set.univ : Set ℂ)) (Set.univ : Set ℂ) := by  have hloc :      TendstoLocallyUniformlyOn        (fun (s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ))) (z : ℂ) =>          ∏ p ∈ s, weierstrassFactor m (z / divisorZeroIndex₀_val p))        (divisorCanonicalProduct m f (Set.univ : Set ℂ))        Filter.atTop (Set.univ : Set ℂ) := by    simpa [HasProdLocallyUniformlyOn] using      (hasProdLocallyUniformlyOn_divisorCanonicalProduct_univ (m := m) (f := f) h_sum)  have hF :      ∀ᶠ s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) in Filter.atTop,        DifferentiableOn ℂ          (fun z : ℂ => ∏ p ∈ s, weierstrassFactor m (z / divisorZeroIndex₀_val p))          (Set.univ : Set ℂ) := by    refine Filter.Eventually.of_forall ?_    intro s    have hdiff :        Differentiable ℂ          (fun z : ℂ => ∏ p ∈ s, weierstrassFactor m (z / divisorZeroIndex₀_val p)) := by      let F : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℂ → ℂ :=        fun p z => weierstrassFactor m (z / divisorZeroIndex₀_val p)      have hF' : ∀ p ∈ s, Differentiable ℂ (F p) := by        intro p hp        have hdiv : Differentiable ℂ (fun z : ℂ => z / divisorZeroIndex₀_val p) := by          have : Differentiable ℂ (fun z : ℂ => z * ((divisorZeroIndex₀_val p)⁻¹)) :=            (differentiable_id : Differentiable ℂ (fun z : ℂ => z)).mul_const              ((divisorZeroIndex₀_val p)⁻¹)          simp [div_eq_mul_inv]        exact (differentiable_weierstrassFactor m).comp hdiv      simpa [F] using (Differentiable.fun_finsetProd (𝕜 := ℂ) (f := F) (u := s) hF')    simpa using hdiff.differentiableOn  haveI : (Filter.atTop : Filter (Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)))).NeBot :=    Filter.atTop_neBot  exact hloc.differentiableOn hF isOpen_univ