no goals
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.116574
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
g : F → G
g' : F →L[𝕜] G
hg : HasStrictFDerivAt g g' (f x)
hf : HasStrictFDerivAt f f' x
⊢ (fun x =>
      ↑g' (((fun p => (f p.fst, f p.snd)) x).fst - ((fun p => (f p.fst, f p.snd)) x).snd) -
        ↑(comp g' f') (x.fst - x.snd)) =o[𝓝 (x, x)]
    fun p => p.fst - p.snd
simpa only [g'.map_sub, f'.coe_comp'] using (g'.isBigO_comp _ _).trans_isLittleO hf