no goals
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.381155
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.381250
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g : E → F
f'✝ f₀' f₁' g' e : E →L[𝕜] F
x : E
s✝ t : Set E
L L₁ L₂ : Filter E
f : E → F
s : Set E
x₀ : E
f' : E →L[𝕜] F
h : HasFDerivWithinAt f f' s x₀
⊢ (fun x => f x - f x₀) =O[𝓝[s] x₀] fun x => x - x₀
simpa only [sub_add_cancel] using h.isBigO.add (isBigO_sub f' (𝓝[s] x₀) x₀)