HasDerivAtZeta0

lemma HasDerivAtZeta0 {N : ℕ} (Npos : 0 < N) {s : ℂ} (reS_pos : 0 < s.re) (s_ne_one : s ≠ 1) :    HasDerivAt (ζ₀ N) (ζ₀' N s) s := by  unfold riemannZeta0 ζ₀'  apply HasDerivAt.fun_sum ?_ |>.add ?_ |>.add ?_ |>.add ?_  · intro n _    convert! hasDerivAt_neg' s |>.const_cpow (c := n) (by aesop) using 1    all_goals (ring_nf; simp [cpow_neg])  · convert! HasDerivAt.comp (h₂ := fun z ↦ -(N : ℂ) ^ z / z) (h := fun z ↦ 1 - z) (h' := -1)      (h₂' := ((N : ℂ) ^ (1 - s) / (1 - s) ^ 2 - Real.log (N : ℝ) * (N : ℂ) ^ (1 - s) / (1 - s)))      (x := s) ?_ ?_ using 1    · ring_nf    · exact HasDerivAt_cpow_over_var N (by rw [sub_ne_zero]; exact s_ne_one.symm)    · convert! hasDerivAt_const s _ |>.sub (hasDerivAt_id _) using 1; simp  · convert! HasDerivAt_neg_cpow_over2 Npos s using 1; simp only [natCast_log, neg_mul, neg_neg]  · simp_rw [div_cpow_eq_cpow_neg, neg_add, ← sub_eq_add_neg]    convert! hasDerivAt_id s |>.mul <| hasDerivAt_Zeta0Integral Npos reS_pos using 1