-- Mathlib/Analysis/Calculus/FDeriv/Comp.lean
theorem HasFDerivAtFilter.comp {g : F → G} {g' : F →L[𝕜] G} {L' : Filter F}
    (hg : HasFDerivAtFilter g g' (f x) L') (hf : HasFDerivAtFilter f f' x L) (hL : Tendsto f L L') :
    HasFDerivAtFilter (g ∘ f) (g'.comp f') x L

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
L : Filter E
g : F → G
g' : F →L[𝕜] G
L' : Filter F
hg : HasFDerivAtFilter g g' (f x) L'
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L'
eq₁ : (fun x' => g' (f x' - f x - f' (x' - x))) =o[L] fun x' => x' - x :=
  IsBigO.trans_isLittleO (isBigO_comp g' (fun x' => f x' - f x - f' (x' - x)) L) (isLittleO hf)
⊢ HasFDerivAtFilter (g ∘ f) (g'.comp f') x L

Tactic:
let eq₂ := (hg.isLittleO.comp_tendsto hL).trans_isBigO hf.isBigO_sub

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
L : Filter E
g : F → G
g' : F →L[𝕜] G
L' : Filter F
hg : HasFDerivAtFilter g g' (f x) L'
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L'
eq₁ : (fun x' => g' (f x' - f x - f' (x' - x))) =o[L] fun x' => x' - x :=
  IsBigO.trans_isLittleO (isBigO_comp g' (fun x' => f x' - f x - f' (x' - x)) L) (isLittleO hf)
eq₂ : ((fun x' => g x' - g (f x) - g' (x' - f x)) ∘ f) =o[L] fun x' => x' - x :=
  IsLittleO.trans_isBigO (IsLittleO.comp_tendsto (isLittleO hg) hL) (isBigO_sub hf)
⊢ HasFDerivAtFilter (g ∘ f) (g'.comp f') x L

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
L : Filter E
g : F → G
g' : F →L[𝕜] G
L' : Filter F
hg : HasFDerivAtFilter g g' (f x) L'
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L'
⊢ HasFDerivAtFilter (g ∘ f) (g'.comp f') x L

Tactic:
let eq₁ := (g'.isBigO_comp _ _).trans_isLittleO hf.isLittleO

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
L : Filter E
g : F → G
g' : F →L[𝕜] G
L' : Filter F
hg : HasFDerivAtFilter g g' (f x) L'
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L'
eq₁ : (fun x' => g' (f x' - f x - f' (x' - x))) =o[L] fun x' => x' - x :=
  IsBigO.trans_isLittleO (isBigO_comp g' (fun x' => f x' - f x - f' (x' - x)) L) (isLittleO hf)
⊢ HasFDerivAtFilter (g ∘ f) (g'.comp f') x L

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
L : Filter E
g : F → G
g' : F →L[𝕜] G
L' : Filter F
hg : HasFDerivAtFilter g g' (f x) L'
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L'
eq₁ : (fun x' => g' (f x' - f x - f' (x' - x))) =o[L] fun x' => x' - x :=
  IsBigO.trans_isLittleO (isBigO_comp g' (fun x' => f x' - f x - f' (x' - x)) L) (isLittleO hf)
eq₂ : ((fun x' => g x' - g (f x) - g' (x' - f x)) ∘ f) =o[L] fun x' => x' - x :=
  IsLittleO.trans_isBigO (IsLittleO.comp_tendsto (isLittleO hg) hL) (isBigO_sub hf)
⊢ HasFDerivAtFilter (g ∘ f) (g'.comp f') x L

Tactic:
refine .of_isLittleO <| eq₂.triangle <| eq₁.congr_left fun x' => ?_

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
L : Filter E
g : F → G
g' : F →L[𝕜] G
L' : Filter F
hg : HasFDerivAtFilter g g' (f x) L'
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L'
eq₁ : (fun x' => g' (f x' - f x - f' (x' - x))) =o[L] fun x' => x' - x :=
  IsBigO.trans_isLittleO (isBigO_comp g' (fun x' => f x' - f x - f' (x' - x)) L) (isLittleO hf)
eq₂ : ((fun x' => g x' - g (f x) - g' (x' - f x)) ∘ f) =o[L] fun x' => x' - x :=
  IsLittleO.trans_isBigO (IsLittleO.comp_tendsto (isLittleO hg) hL) (isBigO_sub hf)
x' : E
⊢ g' (f x' - f x - f' (x' - x)) = g' (f x' - f x) - (g'.comp f') (x' - x)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
L : Filter E
g : F → G
g' : F →L[𝕜] G
L' : Filter F
hg : HasFDerivAtFilter g g' (f x) L'
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L'
eq₁ : (fun x' => g' (f x' - f x - f' (x' - x))) =o[L] fun x' => x' - x :=
  IsBigO.trans_isLittleO (isBigO_comp g' (fun x' => f x' - f x - f' (x' - x)) L) (isLittleO hf)
eq₂ : ((fun x' => g x' - g (f x) - g' (x' - f x)) ∘ f) =o[L] fun x' => x' - x :=
  IsLittleO.trans_isBigO (IsLittleO.comp_tendsto (isLittleO hg) hL) (isBigO_sub hf)
x' : E
⊢ g' (f x' - f x - f' (x' - x)) = g' (f x' - f x) - (g'.comp f') (x' - x)

Tactic:
simp

Result:
no goals