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

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
Tactic:
rfl
State after:
no goals