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

State before:
φ : ℝ → ℂ
a b : ℝ
φDiff : ContDiffOn ℝ 1 φ (uIoo a b)
⊢ ContinuousOn (deriv φ) (uIoo a b)
Tactic:
apply ContDiffOn.continuousOn (𝕜 := ℝ) (n := 0)
State after:
φ : ℝ → ℂ
a b : ℝ
φDiff : ContDiffOn ℝ 1 φ (uIoo a b)
⊢ ContDiffOn ℝ 0 (deriv φ) (uIoo a b)

State before:
φ : ℝ → ℂ
a b : ℝ
φDiff : ContDiffOn ℝ 1 φ (uIoo a b)
⊢ ContDiffOn ℝ 0 (deriv φ) (uIoo a b)
Tactic:
exact (fun h ↦ ((contDiffOn_succ_iff_deriv_of_isOpen isOpen_Ioo).1 h).2) φDiff
State after:
no goals