simp only [f,g, zeta_eq_tsum_one_div_nat_cpow hz, riemannZeta0_apply]
case h
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
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
u_mem : {z | 1 < z.re} ∈ 𝓝 2
z : ℂ
hz : 1 < z.re
⊢ f z = g z
case h
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
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
u_mem : {z | 1 < z.re} ∈ 𝓝 2
z : ℂ
hz : 1 < z.re
⊢ ∑' (n : ℕ), 1 / ↑n ^ z =
    ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ z +
      (-↑N ^ (1 - z) / (1 - z) + -↑N ^ (-z) / 2 + z * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(z + 1)))