Theorem: Tutorial.HasDerivAt.neg (Solution/Advanced/Analysis/Lecture1.lean)

State before:
f : ℝ → ℝ
f' a : ℝ
hf : HasDerivAt f f' a
this : HasDerivAt (fun x => -1 * f x) (-1 * f') a
⊢ HasDerivAt (fun x => -f x) (-f') a
Tactic:
simpa using this
State after:
no goals