Complex.Hadamard.analyticOrderNatAt_divisorCanonicalProduct_zero

lemma analyticOrderNatAt_divisorCanonicalProduct_zero    (m : ℕ) (f : ℂ → ℂ) (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) :    analyticOrderNatAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) 0 = 0 := by  have hcprod_entire :      Differentiable ℂ (divisorCanonicalProduct m f (Set.univ : Set ℂ)) := by    exact differentiable_divisorCanonicalProduct_univ m f h_sum  have hcprod_not_top :      analyticOrderAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) 0 ≠ ⊤ :=    analyticOrderAt_ne_top_of_exists_ne_zero (hf := hcprod_entire)      ⟨0, by simp [divisorCanonicalProduct_zero]⟩ 0  have hcprodA : AnalyticAt ℂ (divisorCanonicalProduct m f (Set.univ : Set ℂ)) 0 :=    hcprod_entire.analyticAt 0  have hcprod0 : divisorCanonicalProduct m f (Set.univ : Set ℂ) 0 ≠ 0 := by    simp [divisorCanonicalProduct_zero]  have : analyticOrderAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) 0 = 0 :=    (hcprodA.analyticOrderAt_eq_zero).2 hcprod0  have hcast :      (analyticOrderNatAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) 0 : ℕ∞) =        analyticOrderAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) 0 :=    Nat.cast_analyticOrderNatAt      (f := divisorCanonicalProduct m f (Set.univ : Set ℂ)) (z₀ := (0 : ℂ)) hcprod_not_top  have :      (analyticOrderNatAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) 0 : ℕ∞) =        0 := by    simp [hcast, this]  exact_mod_cast this