exact fun x _ ↦ by convert LinearDerivative_ofReal x (-1 : ℂ) c; ring
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
⊢ ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
no goals