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
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 : ℕ
refine :
  Tendsto (Prod.map f f) (SProd.sprod (β := Filter E) (𝓝[s] x) (pure x)) (SProd.sprod (β := Filter E) (𝓝[s] x) (pure x))
⊢ HasFDerivWithinAt f^[n] (f' ^ n) s 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
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 : ℕ
⊢ Tendsto (Prod.map f f) (SProd.sprod (β := Filter E) (𝓝[s] x) (pure x)) (SProd.sprod (β := Filter E) (𝓝[s] x) (pure x))

Tactic:
simpa [hx] using hf.continuousWithinAt.tendsto_nhdsWithin hs |>.prodMap (tendsto_pure_pure f x)

Premises used: Filter.tendsto_pure_pure, ContinuousWithinAt.tendsto_nhdsWithin, 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
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasStrictFDerivAt f f' x
hx : f x = x
n : ℕ
⊢ HasStrictFDerivAt f^[n] (f' ^ n) x

Tactic:
HasFDerivAtFilter.iterate hf ?_ n

Premises used: HasStrictFDerivAt, 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 : HasStrictFDerivAt f f' x
hx : f x = x
n : ℕ
refine : Tendsto (Prod.map f f) (𝓝 (x, x)) (𝓝 (x, x))
⊢ HasStrictFDerivAt 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 : HasStrictFDerivAt f f' x
hx : f x = x
n : ℕ
⊢ Tendsto (Prod.map f f) (𝓝 (x, x)) (𝓝 (x, x))

Tactic:
simpa [hx, ContinuousAt] using hf.continuousAt.prodMap' hf.continuousAt

Premises used: ContinuousAt, ContinuousAt.prodMap', HasStrictFDerivAt.continuousAt
-- 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
hf : DifferentiableAt 𝕜 f x
hx : f x = x
n : ℕ
⊢ DifferentiableAt 𝕜 f^[n] x

Tactic:
(hf.hasFDerivAt.iterate hx n).differentiableAt

Premises used: HasFDerivAt.iterate, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- 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
hf : DifferentiableWithinAt 𝕜 f s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ DifferentiableWithinAt 𝕜 f^[n] s x

Tactic:
(hf.hasFDerivWithinAt.iterate hx hs n).differentiableWithinAt

Premises used: HasFDerivWithinAt.iterate, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
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
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
d : E → F →L[𝕜] G
d' : E →L[𝕜] F →L[𝕜] G
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
⊢ HasStrictFDerivAt (fun (y : E) ↦ c y ∘SL d y)
    (HAdd.hAdd (α := E →L[𝕜] F →L[𝕜] H)
      (comp (σ₂₃ := RingHom.id 𝕜) ((compL 𝕜 F G H : (a : G →L[𝕜] H) → (F →L[𝕜] G) →L[𝕜] F →L[𝕜] H) (c x)) d')
      (comp (σ₂₃ := RingHom.id 𝕜)
        ((ContinuousLinearMap.flip (compL 𝕜 F G H) : (a : F →L[𝕜] G) → (G →L[𝕜] H) →L[𝕜] F →L[𝕜] H) (d x)) c'))
    x

Tactic:
(isBoundedBilinearMap_comp.hasStrictFDerivAt (c x, d x)).comp x (hc.prodMk hd)

Premises used: ContinuousLinearMap.comp, HasStrictFDerivAt.prodMk, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
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
s : Set E
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
d : E → F →L[𝕜] G
d' : E →L[𝕜] F →L[𝕜] G
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ HasFDerivWithinAt (fun (y : E) ↦ c y ∘SL d y)
    (HAdd.hAdd (α := E →L[𝕜] F →L[𝕜] H)
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((compL 𝕜 F G H : (a : G →L[𝕜] H) → (F →L[𝕜] G) →L[𝕜] F →L[𝕜] H) (c x)) d')
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((ContinuousLinearMap.flip (compL 𝕜 F G H) : (a : F →L[𝕜] G) → (G →L[𝕜] H) →L[𝕜] F →L[𝕜] H) (d x)) c'))
    s x

Tactic:
(isBoundedBilinearMap_comp.hasFDerivAt (c x, d x)).comp_hasFDerivWithinAt x (hc.prodMk hd)

Premises used: ContinuousLinearMap.comp, HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
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
s : Set E
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
d : E → F →L[𝕜] G
d' : E →L[𝕜] F →L[𝕜] G
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ HasFDerivWithinAt (fun (y : E) ↦ c y ∘SL d y)
    (HAdd.hAdd (α := E →L[𝕜] F →L[𝕜] H)
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((compL 𝕜 F G H : (a : G →L[𝕜] H) → (F →L[𝕜] G) →L[𝕜] F →L[𝕜] H) (c x)) d')
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((ContinuousLinearMap.flip (compL 𝕜 F G H) : (a : F →L[𝕜] G) → (G →L[𝕜] H) →L[𝕜] F →L[𝕜] H) (d x)) c'))
    s x

Tactic:
exact (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x)).comp_hasFDerivWithinAt x (hc.prodMk hd)

Premises used: HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
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
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
d : E → F →L[𝕜] G
d' : E →L[𝕜] F →L[𝕜] G
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
⊢ HasFDerivAt (fun (y : E) ↦ c y ∘SL d y)
    (HAdd.hAdd (α := E →L[𝕜] F →L[𝕜] H)
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((compL 𝕜 F G H : (a : G →L[𝕜] H) → (F →L[𝕜] G) →L[𝕜] F →L[𝕜] H) (c x)) d')
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((ContinuousLinearMap.flip (compL 𝕜 F G H) : (a : F →L[𝕜] G) → (G →L[𝕜] H) →L[𝕜] F →L[𝕜] H) (d x)) c'))
    x

Tactic:
(isBoundedBilinearMap_comp.hasFDerivAt (c x, d x)).comp x <| hc.prodMk hd

Premises used: ContinuousLinearMap.comp, HasFDerivAt.prodMk, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
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
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
d : E → F →L[𝕜] G
d' : E →L[𝕜] F →L[𝕜] G
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
⊢ HasFDerivAt (fun (y : E) ↦ c y ∘SL d y)
    (HAdd.hAdd (α := E →L[𝕜] F →L[𝕜] H)
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((compL 𝕜 F G H : (a : G →L[𝕜] H) → (F →L[𝕜] G) →L[𝕜] F →L[𝕜] H) (c x)) d')
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((ContinuousLinearMap.flip (compL 𝕜 F G H) : (a : F →L[𝕜] G) → (G →L[𝕜] H) →L[𝕜] F →L[𝕜] H) (d x)) c'))
    x

Tactic:
exact (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x)).comp x <| hc.prodMk hd

Premises used: HasFDerivAt.prodMk, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
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
s : Set E
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
d : E → F →L[𝕜] G
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
⊢ DifferentiableWithinAt 𝕜 (F := F →L[𝕜] H) (fun (y : E) ↦ c y ∘SL d y) s x

Tactic:
(hc.hasFDerivWithinAt.clm_comp hd.hasFDerivWithinAt).differentiableWithinAt

Premises used: HasFDerivWithinAt.clm_comp, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
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
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
d : E → F →L[𝕜] G
hc : DifferentiableAt 𝕜 c x
hd : DifferentiableAt 𝕜 d x
⊢ DifferentiableAt 𝕜 (F := F →L[𝕜] H) (fun (y : E) ↦ c y ∘SL d y) x

Tactic:
(hc.hasFDerivAt.clm_comp hd.hasFDerivAt).differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.clm_comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
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
s : Set E
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
d : E → F →L[𝕜] G
hc : DifferentiableOn 𝕜 c s
hd : DifferentiableOn 𝕜 d s
⊢ DifferentiableOn 𝕜 (F := F →L[𝕜] H) (fun (y : E) ↦ c y ∘SL d y) s

Tactic:
fun x hx => (hc x hx).clm_comp (hd x hx)

Premises used: DifferentiableWithinAt.clm_comp, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
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
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
d : E → F →L[𝕜] G
hc : Differentiable 𝕜 c
hd : Differentiable 𝕜 d
⊢ Differentiable 𝕜 (F := F →L[𝕜] H) fun (y : E) ↦ c y ∘SL d y

Tactic:
fun x => (hc x).clm_comp (hd x)

Premises used: Differentiable, DifferentiableAt.clm_comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
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
s : Set E
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
d : E → F →L[𝕜] G
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
⊢ fderivWithin 𝕜 (fun (y : E) ↦ c y ∘SL d y) s x =
    HAdd.hAdd (α := E →L[𝕜] F →L[𝕜] H)
      (comp (σ₂₃ := RingHom.id 𝕜) ((compL 𝕜 F G H : (a : G →L[𝕜] H) → (F →L[𝕜] G) →L[𝕜] F →L[𝕜] H) (c x))
        (fderivWithin 𝕜 d s x))
      (comp (σ₂₃ := RingHom.id 𝕜)
        ((ContinuousLinearMap.flip (compL 𝕜 F G H) : (a : F →L[𝕜] G) → (G →L[𝕜] H) →L[𝕜] F →L[𝕜] H) (d x))
        (fderivWithin 𝕜 c s x))

Tactic:
(hc.hasFDerivWithinAt.clm_comp hd.hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.clm_comp, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
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
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
d : E → F →L[𝕜] G
hc : DifferentiableAt 𝕜 c x
hd : DifferentiableAt 𝕜 d x
⊢ fderiv 𝕜 (fun (y : E) ↦ c y ∘SL d y) x =
    HAdd.hAdd (α := E →L[𝕜] F →L[𝕜] H)
      (comp (σ₂₃ := RingHom.id 𝕜) ((compL 𝕜 F G H : (a : G →L[𝕜] H) → (F →L[𝕜] G) →L[𝕜] F →L[𝕜] H) (c x))
        (fderiv 𝕜 d x))
      (comp (σ₂₃ := RingHom.id 𝕜)
        ((ContinuousLinearMap.flip (compL 𝕜 F G H) : (a : F →L[𝕜] G) → (G →L[𝕜] H) →L[𝕜] F →L[𝕜] H) (d x))
        (fderiv 𝕜 c x))

Tactic:
(hc.hasFDerivAt.clm_comp hd.hasFDerivAt).fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.clm_comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
G : Type u_4
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
x : E
H : Type u_5
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
u : E → G
u' : E →L[𝕜] G
hc : HasStrictFDerivAt c c' x
hu : HasStrictFDerivAt u u' x
⊢ HasStrictFDerivAt (fun (y : E) ↦ (c y : (a : G) → H) (u y))
    (HAdd.hAdd (β := E →L[𝕜] H) (c x ∘SL u') ((c'.flip : (a : G) → E →L[𝕜] H) (u x) : E →L[𝕜] H)) x

Tactic:
(isBoundedBilinearMap_apply.hasStrictFDerivAt (c x, u x)).comp x (hc.prodMk hu)

Premises used: ContinuousLinearMap.comp, HasStrictFDerivAt.prodMk, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
G : Type u_4
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
x : E
s : Set E
H : Type u_5
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
u : E → G
u' : E →L[𝕜] G
hc : HasFDerivWithinAt c c' s x
hu : HasFDerivWithinAt u u' s x
⊢ HasFDerivWithinAt (fun (y : E) ↦ (c y : (a : G) → H) (u y))
    (HAdd.hAdd (β := E →L[𝕜] H) (c x ∘SL u') ((c'.flip : (a : G) → E →L[𝕜] H) (u x) : E →L[𝕜] H)) s x

Tactic:
(isBoundedBilinearMap_apply.hasFDerivAt (c x, u x)).comp_hasFDerivWithinAt x
    (hc.prodMk hu)

Premises used: ContinuousLinearMap.comp, HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
G : Type u_4
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
x : E
s : Set E
H : Type u_5
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
u : E → G
u' : E →L[𝕜] G
hc : HasFDerivWithinAt c c' s x
hu : HasFDerivWithinAt u u' s x
⊢ HasFDerivWithinAt (fun (y : E) ↦ (c y : (a : G) → H) (u y))
    (HAdd.hAdd (β := E →L[𝕜] H) (c x ∘SL u') ((c'.flip : (a : G) → E →L[𝕜] H) (u x) : E →L[𝕜] H)) s x

Tactic:
exact (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x)).comp_hasFDerivWithinAt x
    (hc.prodMk hu)

Premises used: HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
G : Type u_4
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
x : E
H : Type u_5
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
u : E → G
u' : E →L[𝕜] G
hc : HasFDerivAt c c' x
hu : HasFDerivAt u u' x
⊢ HasFDerivAt (fun (y : E) ↦ (c y : (a : G) → H) (u y))
    (HAdd.hAdd (β := E →L[𝕜] H) (c x ∘SL u') ((c'.flip : (a : G) → E →L[𝕜] H) (u x) : E →L[𝕜] H)) x

Tactic:
(isBoundedBilinearMap_apply.hasFDerivAt (c x, u x)).comp x (hc.prodMk hu)

Premises used: ContinuousLinearMap.comp, HasFDerivAt.prodMk, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
G : Type u_4
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
x : E
H : Type u_5
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
u : E → G
u' : E →L[𝕜] G
hc : HasFDerivAt c c' x
hu : HasFDerivAt u u' x
⊢ HasFDerivAt (fun (y : E) ↦ (c y : (a : G) → H) (u y))
    (HAdd.hAdd (β := E →L[𝕜] H) (c x ∘SL u') ((c'.flip : (a : G) → E →L[𝕜] H) (u x) : E →L[𝕜] H)) x

Tactic:
exact (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x)).comp x (hc.prodMk hu)

Premises used: HasFDerivAt.prodMk, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
G : Type u_4
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
x : E
s : Set E
H : Type u_5
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
u : E → G
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
⊢ DifferentiableWithinAt.{u_1, u_2, u_5} 𝕜 (F := H) (fun (y : E) ↦ (c y : (a : G) → H) (u y)) s x

Tactic:
(hc.hasFDerivWithinAt.clm_apply hu.hasFDerivWithinAt).differentiableWithinAt

Premises used: HasFDerivWithinAt.clm_apply, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
G : Type u_4
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
x : E
H : Type u_5
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
u : E → G
hc : DifferentiableAt 𝕜 c x
hu : DifferentiableAt 𝕜 u x
⊢ DifferentiableAt.{u_1, u_2, u_5} 𝕜 (F := H) (fun (y : E) ↦ (c y : (a : G) → H) (u y)) x

Tactic:
(hc.hasFDerivAt.clm_apply hu.hasFDerivAt).differentiableAt

Premises used: HasFDerivAt.clm_apply, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
G : Type u_4
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
s : Set E
H : Type u_5
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
u : E → G
hc : DifferentiableOn 𝕜 c s
hu : DifferentiableOn 𝕜 u s
⊢ DifferentiableOn.{u_1, u_2, u_5} 𝕜 (F := H) (fun (y : E) ↦ (c y : (a : G) → H) (u y)) s

Tactic:
fun x hx => (hc x hx).clm_apply (hu x hx)

Premises used: DifferentiableOn, DifferentiableWithinAt.clm_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
G : Type u_4
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
H : Type u_5
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
u : E → G
hc : Differentiable 𝕜 c
hu : Differentiable 𝕜 u
⊢ Differentiable.{u_1, u_2, u_5} 𝕜 (F := H) fun (y : E) ↦ (c y : (a : G) → H) (u y)

Tactic:
fun x => (hc x).clm_apply (hu x)

Premises used: Differentiable, DifferentiableAt.clm_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
G : Type u_4
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
x : E
s : Set E
H : Type u_5
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
u : E → G
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
⊢ fderivWithin 𝕜 (fun (y : E) ↦ (c y : (a : G) → H) (u y)) s x =
    HAdd.hAdd (α := E →L[𝕜] H) (β := E →L[𝕜] H) (c x ∘SL fderivWithin 𝕜 u s x)
      ((ContinuousLinearMap.flip (fderivWithin 𝕜 c s x) : (a : G) → E →L[𝕜] H) (u x) : E →L[𝕜] H)

Tactic:
(hc.hasFDerivWithinAt.clm_apply hu.hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivWithinAt.clm_apply, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
G : Type u_4
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
x : E
H : Type u_5
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
u : E → G
hc : DifferentiableAt 𝕜 c x
hu : DifferentiableAt 𝕜 u x
⊢ fderiv 𝕜 (fun (y : E) ↦ (c y : (a : G) → H) (u y)) x =
    HAdd.hAdd (α := E →L[𝕜] H) (β := E →L[𝕜] H) (c x ∘SL fderiv 𝕜 u x)
      ((ContinuousLinearMap.flip (fderiv 𝕜 c x) : (a : G) → E →L[𝕜] H) (u x) : E →L[𝕜] H)

Tactic:
(hc.hasFDerivAt.clm_apply hu.hasFDerivAt).fderiv

Premises used: HasFDerivAt.clm_apply, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H
inst_7 : Fintype ι
hc : HasStrictFDerivAt c c' x
u : (i : ι) → M i
⊢ HasStrictFDerivAt.{u_1, u_2, u_7} (𝕜 := 𝕜) (F := H) (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u)
    ((c'.flipMultilinear (E := M) : (a : (i : ι) → M i) → E →L[𝕜] H) u) x

Tactic:
(ContinuousMultilinearMap.apply 𝕜 M H u).hasStrictFDerivAt.comp x hc

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasStrictFDerivAt, HasStrictFDerivAt.comp, LinearMap.mkContinuous, ContinuousMultilinearMap.apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H
inst_7 : Fintype ι
hc : HasFDerivWithinAt c c' s x
u : (i : ι) → M i
⊢ HasFDerivWithinAt.{u_1, u_2, u_7} (𝕜 := 𝕜) (F := H) (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u)
    ((c'.flipMultilinear (E := M) : (a : (i : ι) → M i) → E →L[𝕜] H) u) s x

Tactic:
(ContinuousMultilinearMap.apply 𝕜 M H u).hasFDerivAt.comp_hasFDerivWithinAt x hc

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasFDerivAt, HasFDerivAt.comp_hasFDerivWithinAt, LinearMap.mkContinuous, ContinuousMultilinearMap.apply