Theorem: Tutorial.HasDerivAt.isBigO_sub (Tutorial/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 =>
  sorry
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 =>
  sorry
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:
sorry
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:
sorry
State after:
no goals