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