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

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

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