awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : E [⋀^ι]→L[𝕜] F
x : ι → E
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := F) (⇑f : (a : ι → E) → F) (f.linearDeriv (M₁ := fun (x : ι) ↦ E) x) x

Tactic:
f.1.hasStrictFDerivAt x

Premises used: ContinuousMultilinearMap.hasStrictFDerivAt, ContinuousAlternatingMap.toContinuousMultilinearMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : E [⋀^ι]→L[𝕜] F
x : ι → E
⊢ HasFDerivAt (𝕜 := 𝕜) (F := F) (⇑f : (a : ι → E) → F) (f.linearDeriv (M₁ := fun (x : ι) ↦ E) x) x

Tactic:
f.1.hasFDerivAt x

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : E [⋀^ι]→L[𝕜] F
s : Set (ι → E)
x : ι → E
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := F) (⇑f : (a : ι → E) → F) (f.linearDeriv (M₁ := fun (x : ι) ↦ E) x) s x

Tactic:
(f.hasFDerivAt x).hasFDerivWithinAt

Premises used: HasFDerivAt.hasFDerivWithinAt, ContinuousAlternatingMap.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
f' : E →L[𝕜] F [⋀^ι]→L[𝕜] G
g : ι → E → F
g' : ι → E →L[𝕜] F
x : E
inst_7 : Fintype ι
inst_8 : DecidableEq ι
hf : HasStrictFDerivAt f f' x
hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x
⊢ HasStrictFDerivAt (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x)
    ((apply 𝕜 F G fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ∑ i : ι, (f x).toContinuousLinearMap (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i)
    x

Tactic:
(toContinuousMultilinearMapCLM 𝕜).hasStrictFDerivAt.comp x hf
    |>.continuousMultilinearMap_apply hg

Premises used: ContinuousAlternatingMap.toContinuousLinearMap, HasStrictFDerivAt.continuousMultilinearMap_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
f' : E →L[𝕜] F [⋀^ι]→L[𝕜] G
g : ι → E → F
g' : ι → E →L[𝕜] F
x : E
inst_7 : Fintype ι
inst_8 : DecidableEq ι
hf : HasFDerivAt f f' x
hg : ∀ (i : ι), HasFDerivAt (g i) (g' i) x
⊢ HasFDerivAt (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x)
    ((apply 𝕜 F G fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ∑ i : ι, (f x).toContinuousLinearMap (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i)
    x

Tactic:
(toContinuousMultilinearMapCLM 𝕜).hasFDerivAt.comp x hf
    |>.continuousMultilinearMap_apply hg

Premises used: ContinuousAlternatingMap.toContinuousLinearMap, HasFDerivAt.continuousMultilinearMap_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
f' : E →L[𝕜] F [⋀^ι]→L[𝕜] G
g : ι → E → F
g' : ι → E →L[𝕜] F
s : Set E
x : E
inst_7 : Fintype ι
inst_8 : DecidableEq ι
hf : HasFDerivWithinAt f f' s x
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x
⊢ HasFDerivWithinAt (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x)
    ((apply 𝕜 F G fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ∑ i : ι, (f x).toContinuousLinearMap (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i)
    s x

Tactic:
(toContinuousMultilinearMapCLM 𝕜).hasFDerivAt.comp_hasFDerivWithinAt x hf
    |>.continuousMultilinearMap_apply hg

Premises used: HasFDerivWithinAt.continuousMultilinearMap_apply, ContinuousAlternatingMap.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
s : Set E
x : E
inst_7 : Fintype ι
inst_8 : DecidableEq ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) s x =
    HAdd.hAdd (α := E →L[𝕜] G) ((apply 𝕜 F G fun (x_1 : ι) ↦ g x_1 x) ∘SL fderivWithin 𝕜 f s x)
      (∑ i : ι, (f x).toContinuousLinearMap (fun (x_1 : ι) ↦ g x_1 x) i ∘SL fderivWithin 𝕜 (g i) s x)

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

Premises used: HasFDerivWithinAt.continuousAlternatingMap_apply, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
s : Set E
x : E
inst_7 : Fintype ι
inst_8 : DecidableEq ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
hs : UniqueDiffWithinAt 𝕜 s x
dx : E
⊢ (fderivWithin 𝕜 (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) s x : (a : E) → G) dx =
    HAdd.hAdd (α := G) (β := G)
      ((((fderivWithin 𝕜 f s x : (a : E) → F [⋀^ι]→L[𝕜] G) dx : F [⋀^ι]→L[𝕜] G) : (a : ι → F) → G) fun (x_1 : ι) ↦
          g x_1 x :
        G)
      (∑ i : ι,
          (f x : (a : ι → F) → G)
            (Function.update (β := fun (a : ι) ↦ F) (fun (x_1 : ι) ↦ g x_1 x) i
              ((fderivWithin 𝕜 (g i) s x : (a : E) → F) dx)) :
        G)

Tactic:
simp [fderivWithin_continuousAlternatingMap_apply, *]

Premises used: fderivWithin_continuousAlternatingMap_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
x : E
inst_7 : Fintype ι
inst_8 : DecidableEq ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
⊢ fderiv 𝕜 (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) x =
    HAdd.hAdd (α := E →L[𝕜] G) ((apply 𝕜 F G fun (x_1 : ι) ↦ g x_1 x) ∘SL fderiv 𝕜 f x)
      (∑ i : ι, (f x).toContinuousLinearMap (fun (x_1 : ι) ↦ g x_1 x) i ∘SL fderiv 𝕜 (g i) x)

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

Premises used: HasFDerivAt.continuousAlternatingMap_apply, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
x : E
inst_7 : Fintype ι
inst_8 : DecidableEq ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
dx : E
⊢ (fderiv 𝕜 (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) x : (a : E) → G) dx =
    HAdd.hAdd (α := G) (β := G)
      ((((fderiv 𝕜 f x : (a : E) → F [⋀^ι]→L[𝕜] G) dx : F [⋀^ι]→L[𝕜] G) : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x : G)
      (∑ i : ι,
          (f x : (a : ι → F) → G)
            (Function.update (β := fun (a : ι) ↦ F) (fun (x_1 : ι) ↦ g x_1 x) i ((fderiv 𝕜 (g i) x : (a : E) → F) dx)) :
        G)

Tactic:
simp [fderiv_continuousAlternatingMap_apply, *]

Premises used: fderiv_continuousAlternatingMap_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
s : Set E
x : E
inst_7 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
intro :
  ∀ (val : Fintype ι),
    DifferentiableWithinAt.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) s
      x
⊢ DifferentiableWithinAt.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) s x

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
s : Set E
x : E
inst_7 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
val : Fintype ι
⊢ DifferentiableWithinAt.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) s x

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

Premises used: HasFDerivWithinAt.continuousAlternatingMap_apply, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
s : Set E
x : E
inst_7 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
val : Fintype ι
⊢ DifferentiableWithinAt.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) s x

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

Premises used: HasFDerivWithinAt.continuousAlternatingMap_apply, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
s : Set E
x : E
inst_7 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
val : Fintype ι
⊢ DifferentiableWithinAt.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) s x

Tactic:
classical
  exact hf.hasFDerivWithinAt.continuousAlternatingMap_apply (fun i ↦ (hg i).hasFDerivWithinAt)
    |>.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
x : E
inst_7 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
intro :
  ∀ (val : Fintype ι),
    DifferentiableAt.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) x
⊢ DifferentiableAt.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) x

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
x : E
inst_7 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
val : Fintype ι
⊢ DifferentiableAt.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) x

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

Premises used: HasFDerivAt.continuousAlternatingMap_apply, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
x : E
inst_7 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
val : Fintype ι
⊢ DifferentiableAt.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) x

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

Premises used: HasFDerivAt.continuousAlternatingMap_apply, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
x : E
inst_7 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
val : Fintype ι
⊢ DifferentiableAt.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) x

Tactic:
classical
  exact hf.hasFDerivAt.continuousAlternatingMap_apply (fun i ↦ (hg i).hasFDerivAt)
    |>.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
s : Set E
inst_7 : Finite ι
hf : DifferentiableOn 𝕜 f s
hg : ∀ (i : ι), DifferentiableOn 𝕜 (g i) s
⊢ DifferentiableOn.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) s

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

Premises used: DifferentiableOn, DifferentiableWithinAt.continuousAlternatingMap_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
inst_7 : Finite ι
hf : Differentiable 𝕜 f
hg : ∀ (i : ι), Differentiable 𝕜 (g i)
⊢ Differentiable.{u_1, u_3, u_5} 𝕜 (F := G) fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x

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

Premises used: Differentiable, DifferentiableAt.continuousAlternatingMap_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Finite ι
f : E [⋀^ι]→L[𝕜] F
intro : ∀ (val : Fintype ι), Differentiable 𝕜 (E := ι → E) (F := F) (⇑f : (a : ι → E) → F)
⊢ Differentiable 𝕜 (E := ι → E) (F := F) (⇑f : (a : ι → E) → F)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Finite ι
f : E [⋀^ι]→L[𝕜] F
val : Fintype ι
intro : Differentiable 𝕜 (F := E [⋀^ι]→L[𝕜] F) fun (x : ι → E) ↦ f
intro₁ : ∀ (i : ι), Differentiable 𝕜 (F := E) fun (x : ι → E) ↦ x i
⊢ Differentiable 𝕜 (E := ι → E) (F := F) (⇑f : (a : ι → E) → F)

Tactic:
apply Differentiable.continuousAlternatingMap_apply

Premises used: Differentiable.continuousAlternatingMap_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Finite ι
f : E [⋀^ι]→L[𝕜] F
val : Fintype ι
⊢ Differentiable 𝕜 (F := E [⋀^ι]→L[𝕜] F) fun (x : ι → E) ↦ f

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Finite ι
f : E [⋀^ι]→L[𝕜] F
val : Fintype ι
⊢ ∀ (i : ι), Differentiable 𝕜 (F := E) fun (x : ι → E) ↦ x i

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
Goal:
𝕜 : Type u_1
ι : Type u_2
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → NormedAddCommGroup (F i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
inst_7 : Fintype ι
inst_8 : DecidableEq ι
fg : ContinuousMultilinearMap 𝕜 G H × ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 G H →L[𝕜] ContinuousMultilinearMap 𝕜 F H)
    (⇑(compContinuousLinearMapContinuousMultilinear 𝕜 F G H) :
      (a : (i : ι) → F i →L[𝕜] G i) → ContinuousMultilinearMap 𝕜 G H →L[𝕜] ContinuousMultilinearMap 𝕜 F H)
    (linearDeriv (M₁ := fun (i : ι) ↦ ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))
      (compContinuousLinearMapContinuousMultilinear 𝕜 F G H) fg.2)
    fg.2

Tactic:
have := (compContinuousLinearMapContinuousMultilinear 𝕜 F G H).hasStrictFDerivAt fg.2
-- 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 : HasStrictFDerivAt f f' x
hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x
⊢ HasStrictFDerivAt (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:
hasStrictFDerivAt_compContinuousLinearMap (f x, (g · x))
    |>.comp x (hf.prodMk (hasStrictFDerivAt_pi.2 hg))

Premises used: ContinuousLinearMap.comp, Iff.mpr, HasStrictFDerivAt.prodMk, HasStrictFDerivAt.comp, hasStrictFDerivAt_pi