Complex.differentiableOn_digamma_of_re_gt_norm_lt

theorem differentiableOn_digamma_of_re_gt_norm_lt {a R : ℝ} (ha : 0 < a) (ha1 : a ≤ 1) :    DifferentiableOn ℂ digamma ({z : ℂ | a < z.re} ∩ {z : ℂ | ‖z‖ < R}) := by  set s : Set ℂ := {z : ℂ | a < z.re} ∩ {z : ℂ | ‖z‖ < R}  have hs_open : IsOpen s :=    (isOpen_lt continuous_const continuous_re).inter      (isOpen_lt continuous_norm continuous_const)  have hu : Summable (fun m : ℕ => (R + 1) / (a * ((m : ℝ) + 1) ^ 2)) := by    refine (summable_one_div_natCast_add_one_sq.mul_left ((R + 1) / a)).congr fun m => ?_    rw [mul_one_div, div_div]  have hseries : DifferentiableOn ℂ      (fun z : ℂ => -(Real.eulerMascheroniConstant : ℂ)        + ∑' m : ℕ, (((m : ℂ) + 1)⁻¹ - (z + m)⁻¹)) s := by    refine (differentiableOn_const (-(Real.eulerMascheroniConstant : ℂ))).add ?_    refine differentiableOn_tsum_of_summable_norm hu ?hterm hs_open ?hbound    · intro m z hz      refine DifferentiableAt.differentiableWithinAt ?_      have hden : z + (m : ℂ) ≠ 0 := by        intro hzero        have hza : a < z.re := hz.1        have hpos : 0 < (z + (m : ℂ)).re := by          rw [add_re, natCast_re]          have hm_nonneg : 0 ≤ (m : ℝ) := by positivity          linarith [hza, hm_nonneg]        rw [hzero] at hpos        norm_num at hpos      have hc : DifferentiableAt ℂ (fun _ : ℂ => (((m : ℂ) + 1)⁻¹ : ℂ)) z :=        differentiableAt_const _      have hinv : DifferentiableAt ℂ (fun w : ℂ => (w + (m : ℂ))⁻¹) z :=        (differentiableAt_id.add_const (m : ℂ)).inv hden      simpa [one_div, add_comm] using hc.sub hinv    · intro m z hz      exact norm_inv_add_one_sub_inv_le ha ha1 (le_of_lt hz.1) (le_of_lt hz.2) m  refine hseries.congr fun z hz => ?_  have hpoles : ∀ n : ℕ, z ≠ -(n : ℂ) := by    intro n hzn    have hre := congrArg Complex.re hzn    simp only [neg_re, natCast_re] at hre    have hzpos : 0 < z.re := lt_trans ha hz.1    have hn : 0 ≤ (n : ℝ) := by positivity    linarith  rw [digamma_eq_tsum hpoles]  congr 1  apply tsum_congr  intro n  rw [one_div, one_div, add_comm z (n : ℂ)]