awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
f' : E →L[𝕜] ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
g' : (i : ι) → E →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
x : E
inst_9 : Fintype ι
inst_10 : DecidableEq ι
hf : HasFDerivAt f f' x
hg : ∀ (i : ι), HasFDerivAt (g i) (g' i) x
⊢ HasFDerivAt
    ((fun
          (fg :
            ContinuousMultilinearMap 𝕜 G H ×
              ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))) ↦
        fg.1.compContinuousLinearMap (M₁ := F) (M₁' := G) fg.2) ∘
      fun (x : E) ↦ (f x, fun (i : ι) ↦ g i x))
    (HAdd.hAdd (α :=
        ContinuousMultilinearMap 𝕜 G H ×
            ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) →L[𝕜]
          ContinuousMultilinearMap 𝕜 F H)
        (β :=
        ContinuousMultilinearMap 𝕜 G H ×
            ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) →L[𝕜]
          ContinuousMultilinearMap 𝕜 F H)
        (compContinuousLinearMapL (E := F) (E₁ := G) (f x, fun (x_1 : ι) ↦ g x_1 x).2 ∘SL
            ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 G H)
              ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) :
          ContinuousMultilinearMap 𝕜 G H ×
              ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) →L[𝕜]
            ContinuousMultilinearMap 𝕜 F H)
        ((f x, fun (x_1 : ι) ↦ g x_1 x).1.fderivCompContinuousLinearMap (E := F) (E₁ := G)
              (f x, fun (x_1 : ι) ↦ g x_1 x).2 ∘SL
            ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H)
              ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) :
          ContinuousMultilinearMap 𝕜 G H ×
              ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) →L[𝕜]
            ContinuousMultilinearMap 𝕜 F H) ∘SL
      f'.prod
        (ContinuousLinearMap.pi (φ := fun (i : ι) ↦ ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))
          g'))
    x

Tactic:
hasStrictFDerivAt_compContinuousLinearMap (f x, (g · x)) |>.hasFDerivAt |>.comp x
      (hf.prodMk (hasFDerivAt_pi.2 hg))

Premises used: Iff.mpr, HasFDerivAt.prodMk, hasFDerivAt_pi, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
f' : E →L[𝕜] ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
g' : (i : ι) → E →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
x : E
inst_9 : Fintype ι
inst_10 : DecidableEq ι
hf : HasFDerivAt f f' x
hg : ∀ (i : ι), HasFDerivAt (g i) (g' i) x
⊢ HasFDerivAt (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x)
    ((compContinuousLinearMapL (E := F) (E₁ := G) fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ((f x).fderivCompContinuousLinearMap (E := F) (E₁ := G) fun (x_1 : ι) ↦ g x_1 x) ∘SL
        ContinuousLinearMap.pi (φ := fun (i : ι) ↦ ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))
          g')
    x

Tactic:
convert!
    hasStrictFDerivAt_compContinuousLinearMap (f x, (g · x)) |>.hasFDerivAt |>.comp x
      (hf.prodMk (hasFDerivAt_pi.2 hg))

Premises used: Iff.mpr, HasFDerivAt.prodMk, hasFDerivAt_pi, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
f' : E →L[𝕜] ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
g' : (i : ι) → E →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
s : Set E
x : E
inst_9 : Fintype ι
inst_10 : DecidableEq ι
hf : HasFDerivWithinAt f f' s x
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x
⊢ HasFDerivWithinAt
    ((fun
          (fg :
            ContinuousMultilinearMap 𝕜 G H ×
              ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))) ↦
        fg.1.compContinuousLinearMap (M₁ := F) (M₁' := G) fg.2) ∘
      fun (x : E) ↦ (f x, fun (i : ι) ↦ g i x))
    (HAdd.hAdd (α :=
        ContinuousMultilinearMap 𝕜 G H ×
            ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) →L[𝕜]
          ContinuousMultilinearMap 𝕜 F H)
        (β :=
        ContinuousMultilinearMap 𝕜 G H ×
            ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) →L[𝕜]
          ContinuousMultilinearMap 𝕜 F H)
        (compContinuousLinearMapL (E := F) (E₁ := G) (f x, fun (x_1 : ι) ↦ g x_1 x).2 ∘SL
            ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 G H)
              ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) :
          ContinuousMultilinearMap 𝕜 G H ×
              ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) →L[𝕜]
            ContinuousMultilinearMap 𝕜 F H)
        ((f x, fun (x_1 : ι) ↦ g x_1 x).1.fderivCompContinuousLinearMap (E := F) (E₁ := G)
              (f x, fun (x_1 : ι) ↦ g x_1 x).2 ∘SL
            ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H)
              ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) :
          ContinuousMultilinearMap 𝕜 G H ×
              ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) →L[𝕜]
            ContinuousMultilinearMap 𝕜 F H) ∘SL
      f'.prod
        (ContinuousLinearMap.pi (φ := fun (i : ι) ↦ ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))
          g'))
    s x

Tactic:
hasStrictFDerivAt_compContinuousLinearMap
          (f x, (g · x)) |>.hasFDerivAt |>.comp_hasFDerivWithinAt
      x (hf.prodMk (hasFDerivWithinAt_pi.2 hg))

Premises used: Iff.mpr, HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk, hasFDerivWithinAt_pi
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
f' : E →L[𝕜] ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
g' : (i : ι) → E →L[𝕜] ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
s : Set E
x : E
inst_9 : Fintype ι
inst_10 : DecidableEq ι
hf : HasFDerivWithinAt f f' s x
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x
⊢ HasFDerivWithinAt (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x)
    ((compContinuousLinearMapL (E := F) (E₁ := G) fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ((f x).fderivCompContinuousLinearMap (E := F) (E₁ := G) fun (x_1 : ι) ↦ g x_1 x) ∘SL
        ContinuousLinearMap.pi (φ := fun (i : ι) ↦ ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))
          g')
    s x

Tactic:
convert!
    hasStrictFDerivAt_compContinuousLinearMap
          (f x, (g · x)) |>.hasFDerivAt |>.comp_hasFDerivWithinAt
      x (hf.prodMk (hasFDerivWithinAt_pi.2 hg))

Premises used: Iff.mpr, HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk, hasFDerivWithinAt_pi
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
s : Set E
x : E
inst_9 : Fintype ι
inst_10 : DecidableEq ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) s x =
    HAdd.hAdd (α := E →L[𝕜] ContinuousMultilinearMap 𝕜 F H) (β := E →L[𝕜] ContinuousMultilinearMap 𝕜 F H)
      ((compContinuousLinearMapL (E := F) (E₁ := G) fun (x_1 : ι) ↦ g x_1 x) ∘SL fderivWithin 𝕜 f s x)
      (ContinuousLinearMap.comp (M₂ := (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))
        ((f x).fderivCompContinuousLinearMap (E := F) (E₁ := G) fun (x_1 : ι) ↦ g x_1 x)
        (ContinuousLinearMap.pi (φ := fun (i : ι) ↦ ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))
          fun (i : ι) ↦ fderivWithin 𝕜 (g i) s x))

Tactic:
hf.hasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap
    (fun i ↦ (hg i).hasFDerivWithinAt) |>.fderivWithin hs

Premises used: HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
x : E
inst_9 : Fintype ι
inst_10 : DecidableEq ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
⊢ fderiv 𝕜 (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) x =
    HAdd.hAdd (α := E →L[𝕜] ContinuousMultilinearMap 𝕜 F H) (β := E →L[𝕜] ContinuousMultilinearMap 𝕜 F H)
      ((compContinuousLinearMapL (E := F) (E₁ := G) fun (x_1 : ι) ↦ g x_1 x) ∘SL fderiv 𝕜 f x)
      (ContinuousLinearMap.comp (M₂ := (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))
        ((f x).fderivCompContinuousLinearMap (E := F) (E₁ := G) fun (x_1 : ι) ↦ g x_1 x)
        (ContinuousLinearMap.pi (φ := fun (i : ι) ↦ ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))
          fun (i : ι) ↦ fderiv 𝕜 (g i) x))

Tactic:
hf.hasFDerivAt.continuousMultilinearMapCompContinuousLinearMap
    (fun i ↦ (hg i).hasFDerivAt) |>.fderiv

Premises used: HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
s : Set E
x : E
inst_9 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
intro :
  ∀ (val : Fintype ι),
    DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
      (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) s x
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
    (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) s x

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
s : Set E
x : E
inst_9 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
val : Fintype ι
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
    (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) s x

Tactic:
hf.hasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap
    (fun i ↦ (hg i).hasFDerivWithinAt) |>.differentiableWithinAt

Premises used: HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
s : Set E
x : E
inst_9 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
val : Fintype ι
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
    (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) s x

Tactic:
exact hf.hasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap
    (fun i ↦ (hg i).hasFDerivWithinAt) |>.differentiableWithinAt

Premises used: HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
s : Set E
x : E
inst_9 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
val : Fintype ι
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
    (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) s x

Tactic:
classical
  exact hf.hasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap
    (fun i ↦ (hg i).hasFDerivWithinAt) |>.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
x : E
inst_9 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
intro :
  ∀ (val : Fintype ι),
    DifferentiableAt 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
      (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) x
⊢ DifferentiableAt 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
    (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) x

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
x : E
inst_9 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
val : Fintype ι
⊢ DifferentiableAt 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
    (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) x

Tactic:
hf.hasFDerivAt.continuousMultilinearMapCompContinuousLinearMap
    (fun i ↦ (hg i).hasFDerivAt) |>.differentiableAt

Premises used: HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
x : E
inst_9 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
val : Fintype ι
⊢ DifferentiableAt 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
    (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) x

Tactic:
exact hf.hasFDerivAt.continuousMultilinearMapCompContinuousLinearMap
    (fun i ↦ (hg i).hasFDerivAt) |>.differentiableAt

Premises used: HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
x : E
inst_9 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
val : Fintype ι
⊢ DifferentiableAt 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
    (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) x

Tactic:
classical
  exact hf.hasFDerivAt.continuousMultilinearMapCompContinuousLinearMap
    (fun i ↦ (hg i).hasFDerivAt) |>.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
s : Set E
inst_9 : Finite ι
hf : DifferentiableOn 𝕜 f s
hg : ∀ (i : ι), DifferentiableOn 𝕜 (g i) s
⊢ DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
    (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) s

Tactic:
fun x hx ↦
  (hf x hx).continuousMultilinearMapCompContinuousLinearMap (hg · x hx)

Premises used: DifferentiableOn, DifferentiableWithinAt.continuousMultilinearMapCompContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
inst_9 : Finite ι
hf : Differentiable 𝕜 f
hg : ∀ (i : ι), Differentiable 𝕜 (g i)
⊢ Differentiable 𝕜 (F := ContinuousMultilinearMap 𝕜 F H) fun (x : E) ↦
    (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x

Tactic:
fun x ↦
  (hf x).continuousMultilinearMapCompContinuousLinearMap (hg · x)

Premises used: Differentiable, DifferentiableAt.continuousMultilinearMapCompContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.Defs
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
⊢ HasFDerivAt f f' x ↔
    IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝 x)
      (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x

Tactic:
simp [HasFDerivAt, hasFDerivAtFilter_iff_isLittleOTVS, Function.comp_def]

Premises used: HasFDerivAt, hasFDerivAtFilter_iff_isLittleOTVS, Function.comp_def