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

State before:
f : ℝ → ℝ
f' a✝ a : ℝ
⊢ HasDerivAt id 1 a
Tactic:
rw [hasDerivAt_iff_isLittleO]
State after:
f : ℝ → ℝ
f' a✝ a : ℝ
⊢ (fun x => id x - id a - (x - a) * 1) =o[𝓝 a] fun x => x - a

State before:
f : ℝ → ℝ
f' a✝ a : ℝ
⊢ (fun x => id x - id a - (x - a) * 1) =o[𝓝 a] fun x => x - a
Tactic:
simp
State after:
no goals