Theorem: Zeta0EqZeta (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ ζ₀ N s = ζ s
Tactic:
let f := riemannZeta
State after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
⊢ ζ₀ N s = ζ s

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
⊢ ζ₀ N s = ζ s
Tactic:
let g := ζ₀ N
State after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
⊢ ζ₀ N s = ζ s

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
⊢ ζ₀ N s = ζ s
Tactic:
let U := {z : ℂ | z ≠ 1 ∧ 0 < z.re}
State after:
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

State before:
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
Tactic:
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
State after:
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

State before:
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
Tactic:
have g_an : AnalyticOn ℂ g U := (HolomorphicOn_riemannZeta0 N_pos).analyticOn isOpen_aux
State after:
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
⊢ ζ₀ N s = ζ s

State before:
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
⊢ ζ₀ N s = ζ s
Tactic:
have preconU : IsPreconnected U := by
  apply IsConnected.isPreconnected
  apply (IsOpen.isConnected_iff_isPathConnected isOpen_aux).mp isPathConnected_aux
State after:
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
⊢ ζ₀ N s = ζ s

State before:
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
⊢ ζ₀ N s = ζ s
Tactic:
have h2 : (2 : ℂ) ∈ U := by simp [U]
State after:
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
⊢ ζ₀ N s = ζ s

State before:
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
⊢ ζ₀ N s = ζ s
Tactic:
have s_mem : s ∈ U := by simp [U, reS_pos, s_ne_one]
State after:
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
⊢ ζ₀ N s = ζ s

State before:
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
⊢ ζ₀ N s = ζ s
Tactic:
convert (AnalyticOn.eqOn_of_preconnected_of_eventuallyEq f_an g_an preconU h2 ?_ s_mem).symm
State after:
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

State before:
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
Tactic:
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)
State after:
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

State before:
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
Tactic:
filter_upwards [u_mem]
State after:
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
⊢ ∀ (a : ℂ), 1 < a.re → f a = g a

State before:
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
⊢ ∀ (a : ℂ), 1 < a.re → f a = g a
Tactic:
intro z hz
State after:
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

State before:
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
Tactic:
simp only [f,g, zeta_eq_tsum_one_div_nat_cpow hz, riemannZeta0_apply]
State after:
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)))

State before:
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)))
Tactic:
nth_rewrite 2 [neg_div]
State after:
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)))

State before:
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)))
Tactic:
rw [← sub_eq_add_neg, ← ZetaSum_aux2 N_pos hz, ← sum_add_tsum_nat_add (N + 1) (Summable_rpow hz)]
State after:
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
⊢ ∑ i ∈ Finset.range (N + 1), 1 / ↑i ^ z + ∑' (i : ℕ), 1 / ↑(i + (N + 1)) ^ z =
    ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ z + ∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ z

State before:
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
⊢ ∑ i ∈ Finset.range (N + 1), 1 / ↑i ^ z + ∑' (i : ℕ), 1 / ↑(i + (N + 1)) ^ z =
    ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ z + ∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ z
Tactic:
norm_cast
State after:
no goals

State before:
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}
⊢ AnalyticOn ℂ f U
Tactic:
apply (HolomophicOn_riemannZeta.analyticOn isOpen_ne).mono
State after:
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}
⊢ U ⊆ {s | s ≠ 1}

State before:
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}
⊢ U ⊆ {s | s ≠ 1}
Tactic:
simp only [ne_eq, setOf_subset_setOf, and_imp, U]
State after:
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}
⊢ ∀ (a : ℂ), ¬a = 1 → 0 < a.re → ¬a = 1

State before:
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}
⊢ ∀ (a : ℂ), ¬a = 1 → 0 < a.re → ¬a = 1
Tactic:
exact fun a ha _ ↦ ha
State after:
no goals

State before:
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
⊢ IsPreconnected U
Tactic:
apply IsConnected.isPreconnected
State after:
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
⊢ IsConnected U

State before:
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
⊢ IsConnected U
Tactic:
apply (IsOpen.isConnected_iff_isPathConnected isOpen_aux).mp isPathConnected_aux
State after:
no goals

State before:
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
⊢ 2 ∈ U
Tactic:
simp [U]
State after:
no goals

State before:
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 ∈ U
Tactic:
simp [U, reS_pos, s_ne_one]
State after:
no goals

State before:
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
⊢ {z | 1 < z.re} ∈ 𝓝 2
Tactic:
apply mem_nhds_iff.mpr
State after:
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
⊢ ∃ t ⊆ {z | 1 < z.re}, IsOpen t ∧ 2 ∈ t

State before:
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
⊢ ∃ t ⊆ {z | 1 < z.re}, IsOpen t ∧ 2 ∈ t
Tactic:
use {z : ℂ | 1 < z.re}
State after:
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
⊢ {z | 1 < z.re} ⊆ {z | 1 < z.re} ∧ IsOpen {z | 1 < z.re} ∧ 2 ∈ {z | 1 < z.re}

State before:
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
⊢ {z | 1 < z.re} ⊆ {z | 1 < z.re} ∧ IsOpen {z | 1 < z.re} ∧ 2 ∈ {z | 1 < z.re}
Tactic:
simp only [setOf_subset_setOf, imp_self, forall_const, mem_setOf_eq, re_ofNat,
  Nat.one_lt_ofNat, and_true, true_and]
State after:
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
⊢ IsOpen {z | 1 < z.re}

State before:
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
⊢ IsOpen {z | 1 < z.re}
Tactic:
exact isOpen_lt (by continuity) (by continuity)
State after:
no goals

State before:
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
⊢ Continuous fun z => 1
Tactic:
continuity
State after:
no goals

State before:
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
⊢ Continuous fun z => z.re
Tactic:
continuity
State after:
no goals