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

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

State before:
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x - f a) =O[𝓝 a] fun x => x - a
Tactic:
rw [h.isBigO.congr_of_sub]
State after:
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => (x - a) * f') =O[𝓝 a] fun x => x - a

State before:
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => (x - a) * f') =O[𝓝 a] fun x => x - a
Tactic:
calc (fun x ↦ (x - a) * f')
  _ = fun x ↦ f' * (x - a)  := ?eq1
  _ =O[𝓝 a] fun x ↦ x - a  := ?eq2
State after:
case eq1
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => (x - a) * f') = fun x => f' * (x - a)

case eq2
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => f' * (x - a)) =O[𝓝 a] fun x => x - a

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

State before:
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => f' * (x - a)) =O[𝓝 a] fun x => x - a
Tactic:
case eq2 =>
  apply isBigO_const_mul_self
State after:
no goals

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

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

State before:
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => f' * (x - a)) =O[𝓝 a] fun x => x - a
Tactic:
apply isBigO_const_mul_self
State after:
no goals