Complex.Hadamard.hadamardDenom_ne_zero_at

theorem hadamardDenom_ne_zero_at {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))) {z : ℂ} (hz : f z ≠ 0) : hadamardDenom m f z ≠ 0 := by  have hf_not_top : ∀ w : ℂ, analyticOrderAt f w ≠ ⊤ :=    analyticOrderAt_ne_top_of_exists_ne_zero (hf := hf) hnot  have han_f : AnalyticAt ℂ f z := hf.analyticAt z  have horder_f : analyticOrderNatAt f z = 0 := by    have : analyticOrderAt f z = 0 := (han_f.analyticOrderAt_eq_zero).2 hz    have hcast : (analyticOrderNatAt f z : ℕ∞) = analyticOrderAt f z :=      Nat.cast_analyticOrderNatAt (f := f) (z₀ := z) (hf_not_top z)    have : (analyticOrderNatAt f z : ℕ∞) = 0 := by simp [hcast, this]    exact_mod_cast this  have han_cprod : AnalyticAt ℂ (divisorCanonicalProduct m f (Set.univ : Set ℂ)) z := by    exact analyticAt_divisorCanonicalProduct_univ m f h_sum z  by_cases hz0 : z = 0  · subst hz0    have hord0 : analyticOrderNatAt f 0 = 0 := by simpa using horder_f    simp [hadamardDenom, hord0, divisorCanonicalProduct_zero]  · have hp : z ^ (analyticOrderNatAt f 0) ≠ 0 := pow_ne_zero _ hz0    have hcprod_order :        analyticOrderNatAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) z = 0 := by      simpa [horder_f] using        (analyticOrderNatAt_divisorCanonicalProduct_eq_analyticOrderNatAt (m := m) (hf := hf)          (h_sum := h_sum) (z₀ := z) hz0)    have hcprod_ne : divisorCanonicalProduct m f (Set.univ : Set ℂ) z ≠ 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 ℂ)) z ≠ ⊤ :=        analyticOrderAt_ne_top_of_exists_ne_zero (hf := hcprod_entire)          ⟨0, by simp [divisorCanonicalProduct_zero]⟩ z      have hcprod_cast :          (analyticOrderNatAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) z : ℕ∞) =            analyticOrderAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) z :=        Nat.cast_analyticOrderNatAt          (f := divisorCanonicalProduct m f (Set.univ : Set ℂ)) (z₀ := z) hcprod_not_top      have : analyticOrderAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) z = 0 := by        have :            (analyticOrderNatAt              (divisorCanonicalProduct m f (Set.univ : Set ℂ)) z : ℕ∞) = 0 := by          exact_mod_cast hcprod_order        simp [hcprod_cast] at this        simpa using this      exact (han_cprod.analyticOrderAt_eq_zero).1 this    exact mul_ne_zero hp hcprod_ne