convert LinearDerivative_ofReal x (-1 : ℂ) c
φ : ℝ → ℂ
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 : ℝ
x✝ : x ∈ [[a, b]]
⊢ HasDerivAt u (u' x) x
case h.e'_6.h
φ : ℝ → ℂ
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 : ℝ
x✝¹ : x ∈ [[a, b]]
x✝ : ℝ
⊢ u x✝ = -1 * ↑x✝ + c