awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
inst_6 : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  ContinuousLinearMap.continuousMultilinearMapOption (E := E)
    (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F))
Hf :
  HasStrictFDerivAt
    (fun (x : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
      (f : (a : (i : Option ι) → ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) → F)
        ((fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (x : Option ι) ↦ fx) x))
    ((f.linearDeriv (M₁ := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) fun (x : Option ι) ↦
        fa) ∘SL
      ContinuousLinearMap.pi (φ := fun (i : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
        fun (x : Option ι) ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
e_4 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) Prod.instAddCommGroup
    NormedAddCommGroup.toAddCommGroup
e_5 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    (Prod.instModule : Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) (β :=
    Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    (NormedSpace.toModule : Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
e_6 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) instTopologicalSpaceProd
    UniformSpace.toTopologicalSpace
g : (i : ι) → E i
j : ι
⊢ Function.update (β := E) fa.2 j (g j) j =
    (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
          (fun (x : Option ι) ↦ fa) (some j) (0, g) (some j)).2
      j

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
inst_6 : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  ContinuousLinearMap.continuousMultilinearMapOption (E := E)
    (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F))
Hf :
  HasStrictFDerivAt
    (fun (x : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
      (f : (a : (i : Option ι) → ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) → F)
        ((fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (x : Option ι) ↦ fx) x))
    ((f.linearDeriv (M₁ := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) fun (x : Option ι) ↦
        fa) ∘SL
      ContinuousLinearMap.pi (φ := fun (i : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
        fun (x : Option ι) ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
e_4 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) Prod.instAddCommGroup
    NormedAddCommGroup.toAddCommGroup
e_5 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    (Prod.instModule : Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) (β :=
    Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    (NormedSpace.toModule : Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
e_6 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) instTopologicalSpaceProd
    UniformSpace.toTopologicalSpace
g : (i : ι) → E i
i j : ι
hij : j ≠ i
⊢ Function.update (β := E) fa.2 i (g i) j =
    (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
          (fun (x : Option ι) ↦ fa) (some i) (0, g) (some j)).2
      j

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
G : Type u_4
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id 𝕜) G (E i)
hf : HasStrictFDerivAt f f' x
hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x
⊢ HasStrictFDerivAt
    (fun (x : G) ↦ ((f x, fun (i : ι) ↦ g i x).1 : (a : (i : ι) → E i) → F) (f x, fun (i : ι) ↦ g i x).2)
    (HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i) →L[𝕜] F)
        (apply 𝕜 E F (f x, fun (x_1 : ι) ↦ g x_1 x).2 ∘SL
          ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
        ((f x, fun (x_1 : ι) ↦ g x_1 x).1.linearDeriv (M₁ := E) (f x, fun (x_1 : ι) ↦ g x_1 x).2 ∘SL
          ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) ∘SL
      f'.prod (ContinuousLinearMap.pi (φ := E) g'))
    x

Tactic:
ContinuousMultilinearMap.hasStrictFDerivAt_uncurry (f x, (g · x)) |>.comp x
      (hf.prodMk (hasStrictFDerivAt_pi.2 hg))

Premises used: Iff.mpr, HasStrictFDerivAt.prodMk, HasStrictFDerivAt.comp, hasStrictFDerivAt_pi
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
G : Type u_4
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id 𝕜) G (E i)
hf : HasStrictFDerivAt f f' x
hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x
h :
  (apply 𝕜 E F fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i =
    HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i) →L[𝕜] F)
        (apply 𝕜 E F (f x, fun (x_1 : ι) ↦ g x_1 x).2 ∘SL
          ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
        ((f x, fun (x_1 : ι) ↦ g x_1 x).1.linearDeriv (M₁ := E) (f x, fun (x_1 : ι) ↦ g x_1 x).2 ∘SL
          ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) ∘SL
      f'.prod (ContinuousLinearMap.pi (φ := E) g')
⊢ HasStrictFDerivAt (fun (x : G) ↦ (f x : (a : (i : ι) → E i) → F) fun (x_1 : ι) ↦ g x_1 x)
    ((apply 𝕜 E F fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i)
    x

Tactic:
convert!
    ContinuousMultilinearMap.hasStrictFDerivAt_uncurry (f x, (g · x)) |>.comp x
      (hf.prodMk (hasStrictFDerivAt_pi.2 hg))

Premises used: Iff.mpr, HasStrictFDerivAt.prodMk, HasStrictFDerivAt.comp, hasStrictFDerivAt_pi
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
G : Type u_4
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id 𝕜) G (E i)
hf : HasStrictFDerivAt f f' x
hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x
h :
  ∀ (x_1 : G),
    Eq.{v + 1} (α := F)
      (((apply 𝕜 E F fun (x_2 : ι) ↦ g x_2 x) ∘SL f' +
              ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_2 : ι) ↦ g x_2 x) i ∘SL g' i :
            (a : G) → F)
          x_1 :
        F)
      ((HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i) →L[𝕜] F)
                (apply 𝕜 E F (f x, fun (x_2 : ι) ↦ g x_2 x).2 ∘SL
                  ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
                ((f x, fun (x_2 : ι) ↦ g x_2 x).1.linearDeriv (M₁ := E) (f x, fun (x_2 : ι) ↦ g x_2 x).2 ∘SL
                  ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) ∘SL
              f'.prod (ContinuousLinearMap.pi (φ := E) g') :
            (a : G) → F)
          x_1 :
        F)
⊢ (apply 𝕜 E F fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i =
    HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i) →L[𝕜] F)
        (apply 𝕜 E F (f x, fun (x_1 : ι) ↦ g x_1 x).2 ∘SL
          ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
        ((f x, fun (x_1 : ι) ↦ g x_1 x).1.linearDeriv (M₁ := E) (f x, fun (x_1 : ι) ↦ g x_1 x).2 ∘SL
          ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) ∘SL
      f'.prod (ContinuousLinearMap.pi (φ := E) g')

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
G : Type u_4
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id 𝕜) G (E i)
hf : HasStrictFDerivAt f f' x
hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x
x_1 : G
⊢ Eq.{v + 1} (α := F)
    (((apply 𝕜 E F fun (x_2 : ι) ↦ g x_2 x) ∘SL f' +
            ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_2 : ι) ↦ g x_2 x) i ∘SL g' i :
          (a : G) → F)
        x_1 :
      F)
    ((HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i) →L[𝕜] F)
              (apply 𝕜 E F (f x, fun (x_2 : ι) ↦ g x_2 x).2 ∘SL
                ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
              ((f x, fun (x_2 : ι) ↦ g x_2 x).1.linearDeriv (M₁ := E) (f x, fun (x_2 : ι) ↦ g x_2 x).2 ∘SL
                ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) ∘SL
            f'.prod (ContinuousLinearMap.pi (φ := E) g') :
          (a : G) → F)
        x_1 :
      F)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
G : Type u_4
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id 𝕜) G (E i)
hf : HasFDerivAt f f' x
hg : ∀ (i : ι), HasFDerivAt (g i) (g' i) x
simp :
  ∀ (hf : HasFDerivWithinAt f f' univ x) (hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) univ x),
    HasFDerivWithinAt (fun (x : G) ↦ (f x : (a : (i : ι) → E i) → F) fun (x_1 : ι) ↦ g x_1 x)
      ((apply 𝕜 E F fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
        ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i)
      univ x
⊢ HasFDerivAt (fun (x : G) ↦ (f x : (a : (i : ι) → E i) → F) fun (x_1 : ι) ↦ g x_1 x)
    ((apply 𝕜 E F fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i)
    x

Tactic:
simp only [← hasFDerivWithinAt_univ] at *

Premises used: hasFDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
G : Type u_4
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id 𝕜) G (E i)
hf : HasFDerivWithinAt f f' univ x
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) univ x
⊢ HasFDerivWithinAt (fun (x : G) ↦ (f x : (a : (i : ι) → E i) → F) fun (x_1 : ι) ↦ g x_1 x)
    ((apply 𝕜 E F fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i)
    univ x

Tactic:
hf.continuousMultilinearMap_apply hg

Premises used: HasFDerivWithinAt.continuousMultilinearMap_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
G : Type u_4
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id 𝕜) G (E i)
hf : HasFDerivWithinAt f f' univ x
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) univ x
⊢ HasFDerivWithinAt (fun (x : G) ↦ (f x : (a : (i : ι) → E i) → F) fun (x_1 : ι) ↦ g x_1 x)
    ((apply 𝕜 E F fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i)
    univ x

Tactic:
exact hf.continuousMultilinearMap_apply hg

Premises used: HasFDerivWithinAt.continuousMultilinearMap_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
inst_6 : DecidableEq ι
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
g : (i : ι) → G → E i
g' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id 𝕜) G (E i)
s : Set G
x : G
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x
⊢ HasFDerivWithinAt.{u_1, u_4, v} (𝕜 := 𝕜) (F := F) (fun (x : G) ↦ (f : (a : (i : ι) → E i) → F) fun (i : ι) ↦ g i x)
    (∑ i : ι, f.toContinuousLinearMap (M₁ := E) (fun (j : ι) ↦ g j x) i ∘SL g' i) s x

Tactic:
simpa using (hasFDerivWithinAt_const f x s).continuousMultilinearMap_apply hg

Premises used: HasFDerivWithinAt.continuousMultilinearMap_apply, hasFDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
inst_6 : DecidableEq ι
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
g : (i : ι) → G → E i
g' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id 𝕜) G (E i)
x : G
hg : ∀ (i : ι), HasFDerivAt (g i) (g' i) x
⊢ HasFDerivAt.{u_1, u_4, v} (𝕜 := 𝕜) (F := F) (fun (x : G) ↦ (f : (a : (i : ι) → E i) → F) fun (i : ι) ↦ g i x)
    (∑ i : ι, f.toContinuousLinearMap (M₁ := E) (fun (j : ι) ↦ g j x) i ∘SL g' i) x

Tactic:
simpa using (hasFDerivAt_const f x).continuousMultilinearMap_apply hg

Premises used: hasFDerivAt_const, HasFDerivAt.continuousMultilinearMap_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
ι : Type u_4
inst : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
h'k :
  Membership.mem (α := ι) (γ := Set ι)
    (range (ι := Fin n)
      (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
            ((Equiv.embeddingFinSucc n ι :
                (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
              e)) :
        (a : Fin n) → ι))
    ((e : (a : Fin (n + 1)) → ι) 0 : ι)
⊢ False

Tactic:
simp at h'k
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
ι : Type u_4
inst : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k :
  Membership.mem (α := ι) (γ := Set ι)
    (range (ι := Fin n)
      (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
            ((Equiv.embeddingFinSucc n ι :
                (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
              e)) :
        (a : Fin n) → ι))
    ((e : (a : Fin (n + 1)) → ι) j : ι)
⊢ j ≠ 0

Tactic:
have hj : j ≠ 0 := by
    rintro rfl
    simp at h'k
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
ι : Type u_4
inst : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k :
  Membership.mem (α := ι) (γ := Set ι)
    (range (ι := Fin n)
      (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
            ((Equiv.embeddingFinSucc n ι :
                (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
              e)) :
        (a : Fin n) → ι))
    ((e : (a : Fin (n + 1)) → ι) j : ι)
hj : j ≠ 0
⊢ Eq (α := ι) ((e : (a : Fin (n + 1)) → ι) j : ι)
    ((Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
            ((Equiv.embeddingFinSucc n ι :
                (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
              e) :
          (a : Fin n) → ι)
        (j.pred hj) :
      ι)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
ι : Type u_4
inst : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k :
  Membership.mem (α := ι) (γ := Set ι)
    (range (ι := Fin n)
      (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
            ((Equiv.embeddingFinSucc n ι :
                (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
              e)) :
        (a : Fin n) → ι))
    ((e : (a : Fin (n + 1)) → ι) j : ι)
hj : j ≠ 0
⊢ Eq (α := ι) ((e : (a : Fin (n + 1)) → ι) j : ι)
    ((Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
            ((Equiv.embeddingFinSucc n ι :
                (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
              e) :
          (a : Fin n) → ι)
        (j.pred hj) :
      ι)

Tactic:
have : e j = (Equiv.embeddingFinSucc n ι e).1 (Fin.pred j hj) := by simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
ι : Type u_4
inst : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k :
  Membership.mem (α := ι) (γ := Set ι)
    (range (ι := Fin n)
      (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
            ((Equiv.embeddingFinSucc n ι :
                (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
              e)) :
        (a : Fin n) → ι))
    ((e : (a : Fin (n + 1)) → ι) j : ι)
hj : j ≠ 0
this :
  Eq (α := ι) ((e : (a : Fin (n + 1)) → ι) j : ι)
    ((Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
            ((Equiv.embeddingFinSucc n ι :
                (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
              e) :
          (a : Fin n) → ι)
        (j.pred hj) :
      ι)
⊢ Fin.succ
      (((Equiv.symm
              (Function.Embedding.toEquivRange
                (Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                  ((Equiv.embeddingFinSucc n ι :
                      (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                    e))) :
            (↑(range (ι := Fin n)
                    (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                          ((Equiv.embeddingFinSucc n ι :
                              (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                            e)) :
                      (a : Fin n) → ι)) :
                Type u_4) ≃
              Fin n) :
          (a :
              (↑(range
                    (⇑((Equiv.embeddingFinSucc n ι :
                              (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                            e).fst :
                      (a : Fin n) → ι)) :
                Type u_4)) →
            Fin n)
        (Subtype.mk (p := fun (x : ι) ↦
          Membership.mem (γ := Set ι)
            (range (ι := Fin n)
              (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                    ((Equiv.embeddingFinSucc n ι :
                        (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                      e)) :
                (a : Fin n) → ι))
            x)
          ((Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                ((Equiv.embeddingFinSucc n ι :
                    (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                  e) :
              (a : Fin n) → ι)
            (j.pred hj))
          ⋯)) =
    j

Tactic:
simp [-Equiv.embeddingFinSucc_fst]

Premises used: Equiv.embeddingFinSucc_fst
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
⊢ Eq (α := ((i : ι) → E i) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ (i : ι) → E i) F)
    (iteratedFDeriv 𝕜 n (⇑f : (a : (i : ι) → E i) → F)) (f.iteratedFDeriv (E₁ := E) n)

Tactic:
funext fun x ↦ (f.hasFTaylorSeriesUpTo_iteratedFDeriv.eq_iteratedFDeriv (m := n) le_top x).symm

Premises used: HasFTaylorSeriesUpTo.eq_iteratedFDeriv, ContinuousMultilinearMap.hasFTaylorSeriesUpTo_iteratedFDeriv, funext, le_top, Eq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x : (i : ι) → E i
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ (i : ι) → E i) F) (f.iteratedFDeriv (E₁ := E) n x) ≤
    (↑((Fintype.card ι).descFactorial n) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ (i : ι) → E i) F)
      (iteratedFDeriv 𝕜 n (⇑f : (a : (i : ι) → E i) → F) x) ≤
    (↑((Fintype.card ι).descFactorial n) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)

Tactic:
rw [f.iteratedFDeriv_eq]

Premises used: ContinuousMultilinearMap.iteratedFDeriv_eq