Zeta0EqZeta

@[blueprint  (title := "Zeta0EqZeta")  (statement := /--  For $\Re(s)>0$, $s\ne1$, and for any $N$,  $$  \zeta_0(N,s) = \zeta(s).  $$  -/)  (proof := /-- Use Lemma \ref{ZetaSum_aux2} and the Definition \ref{riemannZeta0}. -/)  (latexEnv := "lemma")]lemma Zeta0EqZeta {N : ℕ} (N_pos : 0 < N) {s : ℂ} (reS_pos : 0 < s.re) (s_ne_one : s ≠ 1) :    ζ₀ N s = riemannZeta s := by  let f := riemannZeta  let g := ζ₀ N  let U := {z : ℂ | z ≠ 1 ∧ 0 < z.re}  have f_an : AnalyticOnNhd ℂ f U := by    apply (HolomorphicOn_riemannZeta.analyticOnNhd isOpen_ne).mono    simp only [ne_eq, setOf_subset_setOf, and_imp, U]    exact fun a ha _ ↦ ha  have g_an : AnalyticOnNhd ℂ g U := (HolomorphicOn_riemannZeta0 N_pos).analyticOnNhd isOpen_aux  have preconU : IsPreconnected U := by    apply IsConnected.isPreconnected    apply (IsOpen.isConnected_iff_isPathConnected isOpen_aux).mpr isPathConnected_aux  have h2 : (2 : ℂ) ∈ U := by simp [U]  have s_mem : s ∈ U := by simp [U, reS_pos, s_ne_one]  convert (AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq f_an g_an preconU h2 ?_ s_mem).symm  have u_mem : {z : ℂ | 1 < z.re} ∈ 𝓝 (2 : ℂ) := by    apply mem_nhds_iff.mpr    use {z : ℂ | 1 < z.re}    simp only [setOf_subset_setOf, imp_self, forall_const, mem_setOf_eq, re_ofNat,      Nat.one_lt_ofNat, and_true, true_and]    exact isOpen_lt (by continuity) (by continuity)  filter_upwards [u_mem]  intro z hz  simp only [f,g, zeta_eq_tsum_one_div_nat_cpow hz, riemannZeta0_apply]  nth_rewrite 2 [neg_div]  rw [← sub_eq_add_neg, ← ZetaSum_aux2 N_pos hz,    ← (summable_one_div_nat_cpow.mpr hz).sum_add_tsum_nat_add (N + 1)]  norm_cast