have f_an : AnalyticOn ℂ f U := by
  apply (HolomophicOn_riemannZeta.analyticOn isOpen_ne).mono
  simp only [ne_eq, setOf_subset_setOf, and_imp, U]
  exact fun a ha _ ↦ ha
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
⊢ ζ₀ N s = ζ s
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
⊢ ζ₀ N s = ζ s