Theorem: ContDiffOn.hasDeriv_deriv (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
φ : ℝ → ℂ
s : Set ℝ
φDiff : ContDiffOn ℝ 1 φ s
x : ℝ
x_in_s : s ∈ 𝓝 x
⊢ 1 ≤ 1
Tactic:
simp
State after:
no goals