Complex.logDeriv_canonicalProduct_one_eq_tsum

theorem logDeriv_canonicalProduct_one_eq_tsum {a : ℕ → ℂ}    (h_sum : Summable (fun n : ℕ => ‖a n‖⁻¹ ^ (2 : ℕ))) (h_nonzero : ∀ n, a n ≠ 0)    {z : ℂ} (hz : z ∉ Set.range a)    (hm : Summable (fun n : ℕ => 1 / (z - a n) + 1 / a n)) :    logDeriv (canonicalProduct 1 a) z =      ∑' n : ℕ, (1 / (z - a n) + 1 / a n) := by  let Φ : ℕ → ℂ → ℂ := fun n w => weierstrassFactor 1 (w / a n)  have hf : ∀ n, Φ n z ≠ 0 := by    intro n    refine weierstrassFactor_ne_zero_of_ne_one 1 ?_    intro h    have hza : z = a n := (div_eq_one_iff_eq (h_nonzero n)).1 h    exact hz ⟨n, hza.symm⟩  have hd : ∀ n, DifferentiableOn ℂ (Φ n) (Set.univ : Set ℂ) := by    intro n    exact ((differentiable_weierstrassFactor 1).comp      (differentiable_id.div_const (a n))).differentiableOn  have hm' : Summable fun n => logDeriv (Φ n) z := by    refine hm.congr ?_    intro n    have hza : z ≠ a n := by      intro h      exact hz ⟨n, h.symm⟩    simpa [Φ] using      (logDeriv_weierstrassFactor_one_div (a := a n) (z := z) (h_nonzero n) hza).symm  have htend : MultipliableLocallyUniformlyOn Φ (Set.univ : Set ℂ) := by    simpa [Φ] using multipliableLocallyUniformlyOn_canonicalProduct h_sum h_nonzero  have hnez : (∏' n, Φ n z) ≠ 0 := by    simpa [Φ, canonicalProduct] using canonicalProduct_ne_zero h_sum h_nonzero hz  have hlog :      logDeriv (∏' n, Φ n ·) z = ∑' n, logDeriv (Φ n) z :=    logDeriv_tprod_eq_tsum (s := (Set.univ : Set ℂ)) isOpen_univ (by simp)      hf hd hm' htend hnez  calc    logDeriv (canonicalProduct 1 a) z = ∑' n, logDeriv (Φ n) z := by      simpa [Φ, canonicalProduct] using! hlog    _ = ∑' n : ℕ, (1 / (z - a n) + 1 / a n) := by      refine tsum_congr fun n => ?_      have hza : z ≠ a n := by        intro h        exact hz ⟨n, h.symm⟩      simpa [Φ] using logDeriv_weierstrassFactor_one_div (a := a n) (z := z) (h_nonzero n) hza