Theorem: DerivZeta0EqDerivZeta (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ deriv (ζ₀ N) s = deriv ζ 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
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
⊢ deriv (ζ₀ N) s = deriv ζ s

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
⊢ deriv (ζ₀ N) s = deriv ζ s
Tactic:
have {x : ℂ} (hx : x ∈ U) : ζ₀ N x = ζ x := by
  simp only [mem_setOf_eq, U] at hx; exact Zeta0EqZeta (N := N) N_pos hx.2 hx.1
State after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
⊢ deriv (ζ₀ N) s = deriv ζ s

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
⊢ deriv (ζ₀ N) s = deriv ζ s
Tactic:
refine deriv_eqOn isOpen_aux ?_ (by simp [U, s_ne_one, reS_pos])
State after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
⊢ ∀ x ∈ {z | z ≠ 1 ∧ 0 < z.re}, HasDerivWithinAt (ζ₀ N) (deriv ζ x) {z | z ≠ 1 ∧ 0 < z.re} x

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
⊢ ∀ x ∈ {z | z ≠ 1 ∧ 0 < z.re}, HasDerivWithinAt (ζ₀ N) (deriv ζ x) {z | z ≠ 1 ∧ 0 < z.re} x
Tactic:
intro x hx
State after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
x : ℂ
hx : x ∈ {z | z ≠ 1 ∧ 0 < z.re}
⊢ HasDerivWithinAt (ζ₀ N) (deriv ζ x) {z | z ≠ 1 ∧ 0 < z.re} x

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
x : ℂ
hx : x ∈ {z | z ≠ 1 ∧ 0 < z.re}
⊢ HasDerivWithinAt (ζ₀ N) (deriv ζ x) {z | z ≠ 1 ∧ 0 < z.re} x
Tactic:
have hζ := HolomophicOn_riemannZeta.mono (by aesop)|>.hasDerivAt (s := U) <| isOpen_aux.mem_nhds hx
State after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
x : ℂ
hx : x ∈ {z | z ≠ 1 ∧ 0 < z.re}
hζ : HasDerivAt ζ (deriv ζ x) x
⊢ HasDerivWithinAt (ζ₀ N) (deriv ζ x) {z | z ≠ 1 ∧ 0 < z.re} x

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
x : ℂ
hx : x ∈ {z | z ≠ 1 ∧ 0 < z.re}
hζ : HasDerivAt ζ (deriv ζ x) x
⊢ HasDerivWithinAt (ζ₀ N) (deriv ζ x) {z | z ≠ 1 ∧ 0 < z.re} x
Tactic:
exact hζ.hasDerivWithinAt.congr (fun y hy ↦ this hy) (this hx)
State after:
no goals

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
x : ℂ
hx : x ∈ U
⊢ ζ₀ N x = ζ x
Tactic:
simp only [mem_setOf_eq, U] at hx
State after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
x : ℂ
hx : x ≠ 1 ∧ 0 < x.re
⊢ ζ₀ N x = ζ x

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
x : ℂ
hx : x ≠ 1 ∧ 0 < x.re
⊢ ζ₀ N x = ζ x
Tactic:
exact Zeta0EqZeta (N := N) N_pos hx.2 hx.1
State after:
no goals

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
⊢ s ∈ {z | z ≠ 1 ∧ 0 < z.re}
Tactic:
simp [U, s_ne_one, reS_pos]
State after:
no goals

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
x : ℂ
hx : x ∈ {z | z ≠ 1 ∧ 0 < z.re}
⊢ U ⊆ {s | s ≠ 1}
Tactic:
aesop
State after:
no goals