awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : HasFDerivAt g g' (f x)
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (g ∘ f) (g' ∘SL f') x

Tactic:
HasFDerivAtFilter.comp hg hf <| hf.continuousAt.tendsto.prodMap <| tendsto_pure_pure ..

Premises used: HasFDerivAt, Filter.tendsto_pure_pure, HasFDerivAtFilter.comp, ContinuousAt.tendsto, 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
x : E
s : Set E
g : F → G
t : Set F
hg : DifferentiableWithinAt 𝕜 g t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
⊢ DifferentiableWithinAt 𝕜 (g ∘ f) s x

Tactic:
(hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h).differentiableWithinAt

Premises used: HasFDerivWithinAt.comp, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- 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
x : E
s : Set E
g : F → G
t : Set F
hg : DifferentiableWithinAt 𝕜 g t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
hg.comp x (hf.mono inter_subset_left) inter_subset_right

Premises used: DifferentiableWithinAt.comp, Set.inter_subset_left, DifferentiableWithinAt.mono, Set.inter_subset_right
-- 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
x : E
f : E → F
g : F → G
hg : DifferentiableAt 𝕜 g (f x)
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt.{u_1, u_2, u_4} 𝕜 (F := G) (fun (x : E) ↦ g (f x)) x

Tactic:
(hg.hasFDerivAt.comp x hf.hasFDerivAt).differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.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
x : E
g : F → G
hg : DifferentiableAt 𝕜 g (f x)
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (g ∘ f) x

Tactic:
(hg.hasFDerivAt.comp x hf.hasFDerivAt).differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.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
x : E
s : Set E
g : F → G
hg : DifferentiableAt 𝕜 g (f x)
hf : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (g ∘ f) s x

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

Premises used: Set.mapsTo_univ, DifferentiableWithinAt.comp, DifferentiableAt.differentiableWithinAt
-- 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
x : E
s : Set E
g : F → G
t : Set F
hg : DifferentiableWithinAt 𝕜 g t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (g ∘ f) s x) (fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x)

Tactic:
(hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.comp, DifferentiableWithinAt.hasFDerivWithinAt
-- 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
x : E
s : Set E
g : F → G
t : Set F
y : F
hg : DifferentiableWithinAt 𝕜 g t y
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hy : f x = y
⊢ DifferentiableWithinAt 𝕜 g t (f x)

Tactic:
subst hy
-- 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
x : E
s : Set E
g : F → G
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (g ∘ f) s x) (fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x)

Tactic:
fderivWithin_comp _ hg hf h hxs

Premises used: fderivWithin_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
x : E
s : Set E
g : F → G
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (g ∘ f) s x) (fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x)

Tactic:
exact fderivWithin_comp _ hg hf h hxs

Premises used: fderivWithin_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
x : E
s : Set E
g : F → G
t : Set F
hg : DifferentiableWithinAt 𝕜 g t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (fun (y : E) ↦ g (f y)) s x) (fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x)

Tactic:
fderivWithin_comp _ hg hf h hxs

Premises used: fderivWithin_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
x : E
s : Set E
g : F → G
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (fun (y : E) ↦ g (f y)) s x) (fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x)

Tactic:
fderivWithin_comp _ hg hf h hxs

Premises used: fderivWithin_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
x : E
s : Set E
g : F → G
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (fun (y : E) ↦ g (f y)) s x) (fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x)

Tactic:
exact fderivWithin_comp _ hg hf h hxs

Premises used: fderivWithin_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
g : F → G
f : E → F
x : E
y : F
s : Set E
t : Set F
hg : DifferentiableWithinAt 𝕜 g t y
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hy : f x = y
v : E
subst :
  ∀ (hg : DifferentiableWithinAt 𝕜 g t (f x)),
    Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
      ((fderivWithin 𝕜 (g ∘ f) s x : (a : E) → G) v : G)
⊢ Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t y : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
    ((fderivWithin 𝕜 (g ∘ f) s x : (a : E) → G) v : G)

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
g : F → G
f : E → F
x : E
s : Set E
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
v : E
hg : DifferentiableWithinAt 𝕜 g t (f x)
rw :
  Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
    ((fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x : (a : E) → G) v : G)
rw₁ :
  Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := F) (⇑(fderivWithin 𝕜 g t (f x)) : (a : F) → G)
        (⇑(fderivWithin 𝕜 f s x) : (a : E) → F) v :
      G)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
    ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
⊢ Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
    ((fderivWithin 𝕜 (g ∘ f) s x : (a : E) → G) v : G)

Tactic:
rw [fderivWithin_comp x hg hf h hxs, coe_comp', Function.comp_apply]

Premises used: ContinuousLinearMap.coe_comp', Function.comp_apply, fderivWithin_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
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
f : E → F
x : E
s : Set E
g' : G → G'
g : F → G
t : Set F
u : Set G
y : F
y' : G
hg' : DifferentiableWithinAt 𝕜 g' u y'
hg : DifferentiableWithinAt 𝕜 g t y
hf : DifferentiableWithinAt 𝕜 f s x
h2g : MapsTo g t u
h2f : MapsTo f s t
h3g : g y = y'
h3f : f x = y
hxs : UniqueDiffWithinAt 𝕜 s x
substs :
  ∀ (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hg' : DifferentiableWithinAt 𝕜 g' u (g (f x))),
    Eq (α := E →L[𝕜] G') (fderivWithin 𝕜 (g' ∘ g ∘ f) s x)
      (fderivWithin 𝕜 g' u (g (f x)) ∘SL fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x)
⊢ Eq (α := E →L[𝕜] G') (fderivWithin 𝕜 (g' ∘ g ∘ f) s x)
    (fderivWithin 𝕜 g' u y' ∘SL fderivWithin 𝕜 g t y ∘SL fderivWithin 𝕜 f s x)

Tactic:
substs h3g h3f
-- 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
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
f : E → F
x : E
s : Set E
g' : G → G'
g : F → G
t : Set F
u : Set G
hf : DifferentiableWithinAt 𝕜 f s x
h2g : MapsTo g t u
h2f : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hg : DifferentiableWithinAt 𝕜 g t (f x)
hg' : DifferentiableWithinAt 𝕜 g' u (g (f x))
⊢ Eq (α := E →L[𝕜] G') (fderivWithin 𝕜 (g' ∘ g ∘ f) s x)
    (fderivWithin 𝕜 g' u (g (f x)) ∘SL fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x)

Tactic:
(hg'.hasFDerivWithinAt.comp x (hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h2f) <|
    h2g.comp h2f).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.comp, Set.MapsTo.comp, DifferentiableWithinAt.hasFDerivWithinAt
-- 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
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
f : E → F
x : E
s : Set E
g' : G → G'
g : F → G
t : Set F
u : Set G
hf : DifferentiableWithinAt 𝕜 f s x
h2g : MapsTo g t u
h2f : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hg : DifferentiableWithinAt 𝕜 g t (f x)
hg' : DifferentiableWithinAt 𝕜 g' u (g (f x))
⊢ Eq (α := E →L[𝕜] G') (fderivWithin 𝕜 (g' ∘ g ∘ f) s x)
    (fderivWithin 𝕜 g' u (g (f x)) ∘SL fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x)

Tactic:
exact (hg'.hasFDerivWithinAt.comp x (hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h2f) <|
    h2g.comp h2f).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.comp, Set.MapsTo.comp, DifferentiableWithinAt.hasFDerivWithinAt
-- 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
x : E
g : F → G
hg : DifferentiableAt 𝕜 g (f x)
hf : DifferentiableAt 𝕜 f x
⊢ Eq (α := E →L[𝕜] G) (fderiv 𝕜 (g ∘ f) x) (fderiv 𝕜 g (f x) ∘SL fderiv 𝕜 f x)

Tactic:
(hg.hasFDerivAt.comp x hf.hasFDerivAt).fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.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
x : E
g : F → G
hg : DifferentiableAt 𝕜 g (f x)
hf : DifferentiableAt 𝕜 f x
⊢ Eq (α := E →L[𝕜] G) (fderiv 𝕜 (fun (y : E) ↦ g (f y)) x) (fderiv 𝕜 g (f x) ∘SL fderiv 𝕜 f x)

Tactic:
fderiv_comp x hg hf

Premises used: fderiv_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
x : E
s : Set E
g : F → G
hg : DifferentiableAt 𝕜 g (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (g ∘ f) s x) (fderiv 𝕜 g (f x) ∘SL fderivWithin 𝕜 f s x)

Tactic:
(hg.hasFDerivAt.comp_hasFDerivWithinAt x hf.hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.fderivWithin, DifferentiableAt.hasFDerivAt, DifferentiableWithinAt.hasFDerivWithinAt
-- 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
s : Set E
g : F → G
t : Set F
hg : DifferentiableOn 𝕜 g t
hf : DifferentiableOn 𝕜 f s
st : MapsTo f s t
⊢ DifferentiableOn.{u_1, u_2, u_4} 𝕜 (F := G) (fun (x : E) ↦ g (f x)) s

Tactic:
fun x hx => DifferentiableWithinAt.comp x (hg (f x) (st hx)) (hf x hx) st

Premises used: DifferentiableWithinAt.comp, DifferentiableOn
-- 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
s : Set E
g : F → G
t : Set F
hg : DifferentiableOn 𝕜 g t
hf : DifferentiableOn 𝕜 f s
st : MapsTo f s t
⊢ DifferentiableOn 𝕜 (g ∘ f) s

Tactic:
fun x hx => DifferentiableWithinAt.comp x (hg (f x) (st hx)) (hf x hx) st

Premises used: DifferentiableWithinAt.comp, DifferentiableOn
-- 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
g : F → G
hg : Differentiable 𝕜 g
hf : Differentiable 𝕜 f
⊢ Differentiable.{u_1, u_2, u_4} 𝕜 (F := G) fun (x : E) ↦ g (f x)

Tactic:
fun x => DifferentiableAt.comp x (hg (f x)) (hf x)

Premises used: Differentiable, DifferentiableAt.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
g : F → G
hg : Differentiable 𝕜 g
hf : Differentiable 𝕜 f
⊢ Differentiable 𝕜 (g ∘ f)

Tactic:
fun x => DifferentiableAt.comp x (hg (f x)) (hf x)

Premises used: Differentiable, DifferentiableAt.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
s : Set E
g : F → G
hg : Differentiable 𝕜 g
hf : DifferentiableOn 𝕜 f s
⊢ DifferentiableOn 𝕜 (g ∘ f) s

Tactic:
hg.differentiableOn.comp hf (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, Differentiable.differentiableOn, DifferentiableOn.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 : E → E
hf : Differentiable 𝕜 f
n : ℕ
⊢ Differentiable 𝕜 f^[n]

Tactic:
Nat.recOn n differentiable_id fun _ ihn => ihn.comp hf

Premises used: Nat.recOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
f : E → E
hf : DifferentiableOn 𝕜 f s
hs : MapsTo f s s
n : ℕ
⊢ DifferentiableOn 𝕜 f^[n] s

Tactic:
Nat.recOn n differentiableOn_id fun _ ihn => ihn.comp hf hs

Premises used: Nat.recOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
⊢ HasFDerivAtFilter f^[0] (HPow.hPow (β := ℕ) f' 0) L

Tactic:
hasFDerivAtFilter_id L

Premises used: ContinuousLinearMap.id, Nat.iterate, npowRec, hasFDerivAtFilter_id
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
⊢ HasFDerivAtFilter f^[0] (HPow.hPow (β := ℕ) f' 0) L

Tactic:
exact hasFDerivAtFilter_id L

Premises used: hasFDerivAtFilter_id
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) L
succ : HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') L
⊢ HasFDerivAtFilter f^[n + 1] (f' ^ (n + 1)) L

Tactic:
rw [Function.iterate_succ, pow_succ]

Premises used: Function.iterate_succ, pow_succ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') L

Tactic:
ihn.comp hf hL

Premises used: HasFDerivAtFilter.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
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') L

Tactic:
exact ihn.comp hf hL

Premises used: HasFDerivAtFilter.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
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
zero : HasFDerivAtFilter f^[0] (HPow.hPow (β := ℕ) f' 0) L
succ : ∀ (n : ℕ) (ihn : HasFDerivAtFilter f^[n] (f' ^ n) L), HasFDerivAtFilter f^[n + 1] (f' ^ (n + 1)) L
⊢ HasFDerivAtFilter f^[n] (f' ^ n) L

Tactic:
induction n with
  | zero => exact hasFDerivAtFilter_id L
  | succ n ihn =>
    rw [Function.iterate_succ, pow_succ]
    exact ihn.comp hf hL

Premises used: Function.iterate_succ, pow_succ, ContinuousLinearMap.zero, hasFDerivAtFilter_id
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAt f f' x
hx : f x = x
n : ℕ
⊢ HasFDerivAt f^[n] (f' ^ n) x

Tactic:
HasFDerivAtFilter.iterate hf ?_ n

Premises used: HasFDerivAt, HasFDerivAtFilter.iterate
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAt f f' x
hx : f x = x
n : ℕ
refine :
  Tendsto (Prod.map f f) (SProd.sprod (β := Filter E) (𝓝 x) (pure x)) (SProd.sprod (β := Filter E) (𝓝 x) (pure x))
⊢ HasFDerivAt f^[n] (f' ^ n) x

Tactic:
refine HasFDerivAtFilter.iterate hf ?_ n

Premises used: HasFDerivAtFilter.iterate
-- Module: Mathlib.Analysis.Calculus.FDeriv.Comp
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAt f f' x
hx : f x = x
n : ℕ
⊢ Tendsto (Prod.map f f) (SProd.sprod (β := Filter E) (𝓝 x) (pure x)) (SProd.sprod (β := Filter E) (𝓝 x) (pure x))

Tactic:
simpa [hx] using hf.continuousAt.tendsto.prodMap (tendsto_pure_pure f x)

Premises used: Filter.tendsto_pure_pure, ContinuousAt.tendsto, 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
x : E
s : Set E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ HasFDerivWithinAt f^[n] (f' ^ n) s x

Tactic:
HasFDerivAtFilter.iterate hf ?_ n

Premises used: HasFDerivWithinAt, HasFDerivAtFilter.iterate