Complex.differentiableAt_digamma_of_re_pos

theorem differentiableAt_digamma_of_re_pos {z₀ : ℂ} (hz₀ : 0 < z₀.re) :    DifferentiableAt ℂ digamma z₀ := by  set a : ℝ := min (z₀.re / 2) 1 with ha_def  set R : ℝ := ‖z₀‖ + 1 with hR_def  have ha : 0 < a := by    rw [ha_def]    exact lt_min (by linarith) one_pos  have ha1 : a ≤ 1 := by    rw [ha_def]    exact min_le_right _ _  have hdiff := differentiableOn_digamma_of_re_gt_norm_lt (a := a) (R := R) ha ha1  have hs_mem :      ({z : ℂ | a < z.re} ∩ {z : ℂ | ‖z‖ < R}) ∈ 𝓝 z₀ := by    have hopen : IsOpen ({z : ℂ | a < z.re} ∩ {z : ℂ | ‖z‖ < R}) :=      (isOpen_lt continuous_const continuous_re).inter        (isOpen_lt continuous_norm continuous_const)    have hzopen : z₀ ∈ ({z : ℂ | a < z.re} ∩ {z : ℂ | ‖z‖ < R}) := by      constructor      · have hale : a ≤ z₀.re / 2 := by          rw [ha_def]          exact min_le_left _ _        exact lt_of_le_of_lt hale (by linarith)      · rw [hR_def]        exact lt_add_of_pos_right ‖z₀‖ (by norm_num : (0 : ℝ) < 1)    exact hopen.mem_nhds hzopen  exact hdiff.differentiableAt hs_mem