Theorem: Tutorial.HasDerivAt.const_mul (Solution/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:
calc (fun x ↦  c * f x - c * f a - (x - a) * (c * f'))
  _ = fun x ↦ c * (f x - f a - (x - a) * f') := ?eq1
  _ =o[𝓝 a] fun x ↦ x - a                   := ?eq2
State after:
case eq1
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')) = fun x => c * (f x - f a - (x - a) * f')

case eq2
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 - f a - (x - a) * 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')) = fun x => c * (f x - f a - (x - a) * f')
Tactic:
case eq1 =>
  funext x
  ring
State after:
no goals

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 - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
Tactic:
case eq2 =>
  apply IsLittleO.const_mul_left hf c
State after:
no goals

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')) = fun x => c * (f x - f a - (x - a) * f')
Tactic:
funext x
State after:
case h
f : ℝ → ℝ
f' a c : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
x : ℝ
⊢ c * f x - c * f a - (x - a) * (c * f') = c * (f x - f a - (x - a) * f')

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

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 - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
Tactic:
apply IsLittleO.const_mul_left hf c
State after:
no goals