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

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
this : HasDerivAt (fun x => f x + -g x) (f' + -g') a
⊢ HasDerivAt (fun x => f x - g x) (f' - g') a
Tactic:
simpa [sub_eq_add_neg] using this
State after:
no goals