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

State before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ (fun h => f (a + h) - f a - h * f') =o[𝓝 0] fun h => h
Tactic:
rw [hasDerivAt_iff_isLittleO, ← map_add_left_nhds_zero a, Asymptotics.isLittleO_map]
State after:
f : ℝ → ℝ
f' a : ℝ
⊢ ((fun x => f x - f a - (x - a) * f') ∘ fun x => a + x) =o[𝓝 0] ((fun x => x - a) ∘ fun x => a + x) ↔
    (fun h => f (a + h) - f a - h * f') =o[𝓝 0] fun h => h