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

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

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