Complex.continuousAt_digamma_of_re_pos

theorem continuousAt_digamma_of_re_pos {z₀ : ℂ} (hz₀ : 0 < z₀.re) :    ContinuousAt 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 hcont := continuousOn_digamma_of_re_ge_norm_le (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 mem_of_superset (hopen.mem_nhds hzopen) fun z hz => by      have hleft : a < z.re := hz.1      have hright : ‖z‖ < R := hz.2      constructor      · exact le_of_lt hleft      · exact le_of_lt hright  exact hcont.continuousAt hs_mem