Theorem: HolomophicOn_riemannZeta (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
⊢ HolomorphicOn ζ {s | s ≠ 1}
Tactic:
intro z hz
State after:
z : ℂ
hz : z ∈ {s | s ≠ 1}
⊢ DifferentiableWithinAt ℂ ζ {s | s ≠ 1} z

State before:
z : ℂ
hz : z ∈ {s | s ≠ 1}
⊢ DifferentiableWithinAt ℂ ζ {s | s ≠ 1} z
Tactic:
simp only [mem_setOf_eq] at hz
State after:
z : ℂ
hz : z ≠ 1
⊢ DifferentiableWithinAt ℂ ζ {s | s ≠ 1} z

State before:
z : ℂ
hz : z ≠ 1
⊢ DifferentiableWithinAt ℂ ζ {s | s ≠ 1} z
Tactic:
exact (differentiableAt_riemannZeta hz).differentiableWithinAt
State after:
no goals