awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
B : E →L[𝕜] F →L[𝕜] G
f : G' → E
g : G' → F
f' : G' →L[𝕜] E
g' : G' →L[𝕜] F
x : G'
s : Set G'
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
⊢ HasFDerivWithinAt (fun (y : G') ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y))
    (HAdd.hAdd (α := G' →L[𝕜] G) (β := G' →L[𝕜] G)
      ((((precompR G' B : (a : E) → (G' →L[𝕜] F) →L[𝕜] G' →L[𝕜] G) (f x) : (G' →L[𝕜] F) →L[𝕜] G' →L[𝕜] G) :
            (a : G' →L[𝕜] F) → G' →L[𝕜] G)
          g' :
        G' →L[𝕜] G)
      ((((precompL G' B : (a : G' →L[𝕜] E) → F →L[𝕜] G' →L[𝕜] G) f' : F →L[𝕜] G' →L[𝕜] G) : (a : F) → G' →L[𝕜] G)
          (g x) :
        G' →L[𝕜] G))
    s x

Tactic:
(B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp_hasFDerivWithinAt x (hf.prodMk hg)

Premises used: ContinuousLinearMap.comp, HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
B : E →L[𝕜] F →L[𝕜] G
f : G' → E
g : G' → F
f' : G' →L[𝕜] E
g' : G' →L[𝕜] F
x : G'
s : Set G'
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
⊢ HasFDerivWithinAt (fun (y : G') ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y))
    (HAdd.hAdd (α := G' →L[𝕜] G) (β := G' →L[𝕜] G)
      ((((precompR G' B : (a : E) → (G' →L[𝕜] F) →L[𝕜] G' →L[𝕜] G) (f x) : (G' →L[𝕜] F) →L[𝕜] G' →L[𝕜] G) :
            (a : G' →L[𝕜] F) → G' →L[𝕜] G)
          g' :
        G' →L[𝕜] G)
      ((((precompL G' B : (a : G' →L[𝕜] E) → F →L[𝕜] G' →L[𝕜] G) f' : F →L[𝕜] G' →L[𝕜] G) : (a : F) → G' →L[𝕜] G)
          (g x) :
        G' →L[𝕜] G))
    s x

Tactic:
exact (B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp_hasFDerivWithinAt x (hf.prodMk hg)

Premises used: HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
B : E →L[𝕜] F →L[𝕜] G
f : G' → E
g : G' → F
f' : G' →L[𝕜] E
g' : G' →L[𝕜] F
x : G'
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
⊢ HasFDerivAt (fun (y : G') ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y))
    (HAdd.hAdd (α := G' →L[𝕜] G) (β := G' →L[𝕜] G)
      ((((precompR G' B : (a : E) → (G' →L[𝕜] F) →L[𝕜] G' →L[𝕜] G) (f x) : (G' →L[𝕜] F) →L[𝕜] G' →L[𝕜] G) :
            (a : G' →L[𝕜] F) → G' →L[𝕜] G)
          g' :
        G' →L[𝕜] G)
      ((((precompL G' B : (a : G' →L[𝕜] E) → F →L[𝕜] G' →L[𝕜] G) f' : F →L[𝕜] G' →L[𝕜] G) : (a : F) → G' →L[𝕜] G)
          (g x) :
        G' →L[𝕜] G))
    x

Tactic:
(B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp x (hf.prodMk hg)

Premises used: ContinuousLinearMap.comp, HasFDerivAt.prodMk, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
B : E →L[𝕜] F →L[𝕜] G
f : G' → E
g : G' → F
f' : G' →L[𝕜] E
g' : G' →L[𝕜] F
x : G'
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
⊢ HasFDerivAt (fun (y : G') ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y))
    (HAdd.hAdd (α := G' →L[𝕜] G) (β := G' →L[𝕜] G)
      ((((precompR G' B : (a : E) → (G' →L[𝕜] F) →L[𝕜] G' →L[𝕜] G) (f x) : (G' →L[𝕜] F) →L[𝕜] G' →L[𝕜] G) :
            (a : G' →L[𝕜] F) → G' →L[𝕜] G)
          g' :
        G' →L[𝕜] G)
      ((((precompL G' B : (a : G' →L[𝕜] E) → F →L[𝕜] G' →L[𝕜] G) f' : F →L[𝕜] G' →L[𝕜] G) : (a : F) → G' →L[𝕜] G)
          (g x) :
        G' →L[𝕜] G))
    x

Tactic:
exact (B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp x (hf.prodMk hg)

Premises used: HasFDerivAt.prodMk, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
B : E →L[𝕜] F →L[𝕜] G
f : G' → E
g : G' → F
f' : G' →L[𝕜] E
g' : G' →L[𝕜] F
x : G'
hf : HasStrictFDerivAt f f' x
hg : HasStrictFDerivAt g g' x
⊢ HasStrictFDerivAt (fun (y : G') ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y))
    (HAdd.hAdd (α := G' →L[𝕜] G) (β := G' →L[𝕜] G)
      ((((precompR G' B : (a : E) → (G' →L[𝕜] F) →L[𝕜] G' →L[𝕜] G) (f x) : (G' →L[𝕜] F) →L[𝕜] G' →L[𝕜] G) :
            (a : G' →L[𝕜] F) → G' →L[𝕜] G)
          g' :
        G' →L[𝕜] G)
      ((((precompL G' B : (a : G' →L[𝕜] E) → F →L[𝕜] G' →L[𝕜] G) f' : F →L[𝕜] G' →L[𝕜] G) : (a : F) → G' →L[𝕜] G)
          (g x) :
        G' →L[𝕜] G))
    x

Tactic:
(B.isBoundedBilinearMap.hasStrictFDerivAt (f x, g x)).comp x (hf.prodMk hg)

Premises used: ContinuousLinearMap.comp, HasStrictFDerivAt.prodMk, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
B : E →L[𝕜] F →L[𝕜] G
f : G' → E
g : G' → F
x : G'
s : Set G'
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun (y : G') ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) s x =
    HAdd.hAdd (α := G' →L[𝕜] G) (β := G' →L[𝕜] G)
      ((((precompR G' B : (a : E) → (G' →L[𝕜] F) →L[𝕜] G' →L[𝕜] G) (f x) : (G' →L[𝕜] F) →L[𝕜] G' →L[𝕜] G) :
            (a : G' →L[𝕜] F) → G' →L[𝕜] G)
          (fderivWithin 𝕜 g s x) :
        G' →L[𝕜] G)
      ((((precompL G' B : (a : G' →L[𝕜] E) → F →L[𝕜] G' →L[𝕜] G) (fderivWithin 𝕜 f s x) : F →L[𝕜] G' →L[𝕜] G) :
            (a : F) → G' →L[𝕜] G)
          (g x) :
        G' →L[𝕜] G)

Tactic:
(B.hasFDerivWithinAt_of_bilinear hf.hasFDerivWithinAt hg.hasFDerivWithinAt).fderivWithin hs

Premises used: ContinuousLinearMap.hasFDerivWithinAt_of_bilinear, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
B : E →L[𝕜] F →L[𝕜] G
f : G' → E
g : G' → F
x : G'
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
⊢ fderiv 𝕜 (fun (y : G') ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) x =
    HAdd.hAdd (α := G' →L[𝕜] G) (β := G' →L[𝕜] G)
      ((((precompR G' B : (a : E) → (G' →L[𝕜] F) →L[𝕜] G' →L[𝕜] G) (f x) : (G' →L[𝕜] F) →L[𝕜] G' →L[𝕜] G) :
            (a : G' →L[𝕜] F) → G' →L[𝕜] G)
          (fderiv 𝕜 g x) :
        G' →L[𝕜] G)
      ((((precompL G' B : (a : G' →L[𝕜] E) → F →L[𝕜] G' →L[𝕜] G) (fderiv 𝕜 f x) : F →L[𝕜] G' →L[𝕜] G) :
            (a : F) → G' →L[𝕜] G)
          (g x) :
        G' →L[𝕜] G)

Tactic:
(B.hasFDerivAt_of_bilinear hf.hasFDerivAt hg.hasFDerivAt).fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, ContinuousLinearMap.hasFDerivAt_of_bilinear
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
h :
  ∀ (x : E × E),
    HSub.hSub (β := G) ((g ∘ f) x.1 - (g ∘ f) x.2) ((g' ∘SL f' : (a : E) → G) (x.1 - x.2) : G) =
      HAdd.hAdd (β := G) (HSub.hSub (β := G) (g (f x.1) - g (f x.2)) ((g' : (a : F) → G) (f x.1 - f x.2) : G))
        ((g' : (a : F) → G) (HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)) : G)
⊢ Eq (α := (p : E × E) → G)
    (fun (p : E × E) ↦ HSub.hSub (β := G) ((g ∘ f) p.1 - (g ∘ f) p.2) ((g' ∘SL f' : (a : E) → G) (p.1 - p.2) : G))
    fun (p : E × E) ↦
    HAdd.hAdd (β := G) (HSub.hSub (β := G) (g (f p.1) - g (f p.2)) ((g' : (a : F) → G) (f p.1 - f p.2) : G))
      ((g' : (a : F) → G) (HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)) : G)

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
x : E × E
⊢ HSub.hSub (β := G) ((g ∘ f) x.1 - (g ∘ f) x.2) ((g' ∘SL f' : (a : E) → G) (x.1 - x.2) : G) =
    HAdd.hAdd (β := G) (HSub.hSub (β := G) (g (f x.1) - g (f x.2)) ((g' : (a : F) → G) (f x.1 - f x.2) : G))
      ((g' : (a : F) → G) (HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)) : G)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
refine :
  IsLittleOTVS.{u_1, u_2, u_4, u_2} 𝕜 (E := G) (F := E) L
    (fun (p : E × E) ↦ HSub.hSub (β := G) (g (f p.1) - g (f p.2)) ((g' : (a : F) → G) (f p.1 - f p.2) : G))
    fun (p : E × E) ↦ p.1 - p.2
refine₁ :
  IsLittleOTVS.{u_1, u_2, u_4, u_2} 𝕜 (E := G) (F := E) L
    (fun (p : E × E) ↦ (g' : (a : F) → G) (HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)))
    fun (p : E × E) ↦ p.1 - p.2
⊢ HasFDerivAtFilter (g ∘ f) (g' ∘SL f') L

Tactic:
refine .of_isLittleOTVS <| calc
    (fun p ↦ (g ∘ f) p.1 - (g ∘ f) p.2 - (g' ∘L f') (p.1 - p.2))
      = fun p ↦ (g (f p.1) - g (f p.2) - g' (f p.1 - f p.2)) +
          g' (f p.1 - f p.2 - f' (p.1 - p.2)) := by
      ext; simp
    _ =o[𝕜; L] (fun p ↦ p.1 - p.2) := .add ?Hg ?Hf

Premises used: ContinuousLinearMap.comp, HSub.hSub, Function.comp, HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ IsLittleOTVS.{u_1, u_2, u_4, u_3} 𝕜 (E := G) (F := F) L
    (fun (p : E × E) ↦ HSub.hSub (β := G) (g (f p.1) - g (f p.2)) ((g' : (a : F) → G) (f p.1 - f p.2) : G))
    fun (p : E × E) ↦ f p.1 - f p.2

Tactic:
hg.isLittleOTVS.comp_tendsto hL

Premises used: Asymptotics.IsLittleOTVS.comp_tendsto, HasFDerivAtFilter.isLittleOTVS
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ IsBigOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) L (fun (p : E × E) ↦ f p.1 - f p.2) fun (p : E × E) ↦ p.1 - p.2

Tactic:
hf.isBigOTVS_sub

Premises used: HasFDerivAtFilter.isBigOTVS_sub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ IsLittleOTVS.{u_1, u_2, u_4, u_2} 𝕜 (E := G) (F := E) L
    (fun (p : E × E) ↦ HSub.hSub (β := G) (g (f p.1) - g (f p.2)) ((g' : (a : F) → G) (f p.1 - f p.2) : G))
    fun (p : E × E) ↦ p.1 - p.2

Tactic:
calc (fun p ↦ g (f p.1) - g (f p.2) - g' (f p.1 - f p.2))
    _ =o[𝕜; L] (fun p ↦ f p.1 - f p.2) :=
      hg.isLittleOTVS.comp_tendsto hL
    _ =O[𝕜; L] (fun p ↦ p.1 - p.2) := hf.isBigOTVS_sub

Premises used: HasFDerivAtFilter.isBigOTVS_sub, HSub.hSub, Asymptotics.IsLittleOTVS.comp_tendsto, HasFDerivAtFilter.isLittleOTVS, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ IsLittleOTVS.{u_1, u_2, u_4, u_2} 𝕜 (E := G) (F := E) L
    (fun (p : E × E) ↦ HSub.hSub (β := G) (g (f p.1) - g (f p.2)) ((g' : (a : F) → G) (f p.1 - f p.2) : G))
    fun (p : E × E) ↦ p.1 - p.2

Tactic:
case Hg => calc (fun p ↦ g (f p.1) - g (f p.2) - g' (f p.1 - f p.2))
    _ =o[𝕜; L] (fun p ↦ f p.1 - f p.2) :=
      hg.isLittleOTVS.comp_tendsto hL
    _ =O[𝕜; L] (fun p ↦ p.1 - p.2) := hf.isBigOTVS_sub

Premises used: HasFDerivAtFilter.isBigOTVS_sub, HSub.hSub, Asymptotics.IsLittleOTVS.comp_tendsto, HasFDerivAtFilter.isLittleOTVS, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ IsBigOTVS.{u_1, u_2, u_4, u_3} 𝕜 (E := G) (F := F) L
    (fun (p : E × E) ↦ (g' : (a : F) → G) (HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)))
    fun (p : E × E) ↦ HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)

Tactic:
g'.isBigOTVS_comp

Premises used: ContinuousLinearMap.isBigOTVS_comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) L
    (fun (p : E × E) ↦ HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)) fun (p : E × E) ↦
    p.1 - p.2

Tactic:
hf.isLittleOTVS

Premises used: HasFDerivAtFilter.isLittleOTVS
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ IsLittleOTVS.{u_1, u_2, u_4, u_2} 𝕜 (E := G) (F := E) L
    (fun (p : E × E) ↦ (g' : (a : F) → G) (HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)))
    fun (p : E × E) ↦ p.1 - p.2

Tactic:
calc (fun p ↦ g' (f p.1 - f p.2 - f' (p.1 - p.2)))
    _ =O[𝕜; L] (fun p ↦ f p.1 - f p.2 - f' (p.1 - p.2)) := g'.isBigOTVS_comp
    _ =o[𝕜; L] (fun p ↦ p.1 - p.2) := hf.isLittleOTVS

Premises used: HSub.hSub, ContinuousLinearMap.isBigOTVS_comp, HasFDerivAtFilter.isLittleOTVS, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ IsLittleOTVS.{u_1, u_2, u_4, u_2} 𝕜 (E := G) (F := E) L
    (fun (p : E × E) ↦ (g' : (a : F) → G) (HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)))
    fun (p : E × E) ↦ p.1 - p.2

Tactic:
case Hf => calc (fun p ↦ g' (f p.1 - f p.2 - f' (p.1 - p.2)))
    _ =O[𝕜; L] (fun p ↦ f p.1 - f p.2 - f' (p.1 - p.2)) := g'.isBigOTVS_comp
    _ =o[𝕜; L] (fun p ↦ p.1 - p.2) := hf.isLittleOTVS

Premises used: HSub.hSub, ContinuousLinearMap.isBigOTVS_comp, HasFDerivAtFilter.isLittleOTVS, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
g : F → G
g' : F →L[𝕜] G
hg : HasStrictFDerivAt g g' (f x)
hf : HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt (fun (x : E) ↦ g (f x)) (g' ∘SL f') x

Tactic:
HasFDerivAtFilter.comp hg hf <| hf.continuousAt.tendsto.prodMap_nhds hf.continuousAt.tendsto

Premises used: HasFDerivAtFilter.comp, ContinuousAt.tendsto, HasStrictFDerivAt, HasStrictFDerivAt.continuousAt, Filter.Tendsto.prodMap_nhds
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
g : F → G
g' : F →L[𝕜] G
t : Set F
hg : HasFDerivWithinAt g g' t (f x)
hf : HasFDerivWithinAt f f' s x
hst : MapsTo f s t
⊢ HasFDerivWithinAt (g ∘ f) (g' ∘SL f') s x

Tactic:
HasFDerivAtFilter.comp hg hf <| .prodMap (hf.continuousWithinAt.tendsto_nhdsWithin hst) <|
    tendsto_pure_pure ..

Premises used: Filter.tendsto_pure_pure, HasFDerivWithinAt, ContinuousWithinAt.tendsto_nhdsWithin, HasFDerivAtFilter.comp, HasFDerivWithinAt.continuousWithinAt, Filter.Tendsto.prodMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
g : F → G
g' : F →L[𝕜] G
hg : HasFDerivAt g g' (f x)
hf : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (g ∘ f) (g' ∘SL f') s x

Tactic:
hg.hasFDerivWithinAt.comp x hf (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, HasFDerivAt.hasFDerivWithinAt, HasFDerivWithinAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
g : F → G
g' : F →L[𝕜] G
t : Set F
hg : HasFDerivWithinAt g g' t (f x)
hf : HasFDerivWithinAt f f' s x
hst : Tendsto f (𝓝[s] x) (𝓝[t] f x)
⊢ HasFDerivWithinAt (g ∘ f) (g' ∘SL f') s x

Tactic:
HasFDerivAtFilter.comp hg hf <| hst.prodMap <| tendsto_pure_pure ..

Premises used: Filter.tendsto_pure_pure, HasFDerivWithinAt, HasFDerivAtFilter.comp, Filter.Tendsto.prodMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
g : F → G
g' : F →L[𝕜] G
t : Set F
hg : HasFDerivWithinAt g g' t (f x)
hf : HasFDerivAt f f' x
ht : ∀ᶠ (x' : E) in 𝓝 x, f x' ∈ t
⊢ HasFDerivAt (g ∘ f) (g' ∘SL f') x

Tactic:
HasFDerivAtFilter.comp hg hf <| .prodMap (tendsto_nhdsWithin_iff.mpr ⟨hf.continuousAt, ht⟩) <|
    tendsto_pure_pure ..

Premises used: Iff.mpr, HasFDerivAt, tendsto_nhdsWithin_iff, Filter.tendsto_pure_pure, HasFDerivAtFilter.comp, And.intro, HasFDerivAt.continuousAt, Filter.Tendsto.prodMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
g : F → G
g' : F →L[𝕜] G
t : Set F
y : F
hg : HasFDerivWithinAt g g' t y
hf : HasFDerivAt f f' x
ht : ∀ᶠ (x' : E) in 𝓝 x, f x' ∈ t
hy : y = f x
⊢ HasFDerivWithinAt g g' t (f x)

Tactic:
subst y
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
g : F → G
g' : F →L[𝕜] G
t : Set F
hf : HasFDerivAt f f' x
ht : ∀ᶠ (x' : E) in 𝓝 x, f x' ∈ t
hg : HasFDerivWithinAt g g' t (f x)
⊢ HasFDerivAt (g ∘ f) (g' ∘SL f') x

Tactic:
hg.comp_hasFDerivAt x hf ht

Premises used: HasFDerivWithinAt.comp_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
g : F → G
g' : F →L[𝕜] G
t : Set F
hf : HasFDerivAt f f' x
ht : ∀ᶠ (x' : E) in 𝓝 x, f x' ∈ t
hg : HasFDerivWithinAt g g' t (f x)
⊢ HasFDerivAt (g ∘ f) (g' ∘SL f') x

Tactic:
exact hg.comp_hasFDerivAt x hf ht

Premises used: HasFDerivWithinAt.comp_hasFDerivAt