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)
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
⊢ f =ᶠ[𝓝 2] g
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
⊢ f =ᶠ[𝓝 2] g