Theorem: DifferentiableAt.isBigO_of_eq_zero (EulerProducts/PNT.lean)

State before:
f : ℂ → ℂ
z : ℂ
hf : DifferentiableAt ℂ f z
hz : f z = 0
⊢ (fun w => f (w + z)) =O[𝓝 0] id
Tactic:
rw [← zero_add z] at hf
State after:
f : ℂ → ℂ
z : ℂ
hf : DifferentiableAt ℂ f (0 + z)
hz : f z = 0
⊢ (fun w => f (w + z)) =O[𝓝 0] id

State before:
f : ℂ → ℂ
z : ℂ
hf : DifferentiableAt ℂ f (0 + z)
hz : f z = 0
⊢ (fun w => f (w + z)) =O[𝓝 0] id
Tactic:
simpa only [zero_add, hz, sub_zero]
  using (hf.hasDerivAt.comp_add_const 0 z).differentiableAt.isBigO_sub
State after:
no goals