have {x : ℂ} (hx : x ∈ U) : ζ₀ N x = ζ x := by
  simp only [mem_setOf_eq, U] at hx; exact Zeta0EqZeta (N := N) N_pos hx.2 hx.1
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
⊢ deriv (ζ₀ N) s = deriv ζ s
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
⊢ deriv (ζ₀ N) s = deriv ζ s