awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
F : Type u_4
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
inst_7 : Fintype ι
inst_8 : DecidableEq ι
fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)
rw :
  HasStrictFDerivAt
    (toContinuousMultilinearMap ∘ fun (fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)) ↦ fg.1.compContinuousLinearMap fg.2)
    (toContinuousMultilinearMapCLM 𝕜 ∘SL
      HAdd.hAdd (α := G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H) (β :=
        G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
        (compContinuousLinearMapCLM fg.2 ∘SL ContinuousLinearMap.fst 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
          G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
        (fg.1.fderivCompContinuousLinearMap fg.2 ∘SL ContinuousLinearMap.snd 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
          G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H))
    fg
⊢ HasStrictFDerivAt (fun (fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)) ↦ fg.1.compContinuousLinearMap fg.2)
    (HAdd.hAdd (α := G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H) (β :=
      G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
      (compContinuousLinearMapCLM fg.2 ∘SL ContinuousLinearMap.fst 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
        G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
      (fg.1.fderivCompContinuousLinearMap fg.2 ∘SL ContinuousLinearMap.snd 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
        G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H))
    fg

Tactic:
rw [← hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff]

Premises used: ContinuousAlternatingMap.hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
F : Type u_4
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
inst_7 : Fintype ι
inst_8 : DecidableEq ι
fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)
⊢ HasStrictFDerivAt
    (fun (fg : ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G)) ↦
      fg.1.compContinuousLinearMap (M₁ := fun (x : ι) ↦ F) (M₁' := fun (x : ι) ↦ G) fg.2)
    (HAdd.hAdd (α :=
      ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
        ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
      (β :=
      ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
        ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
      (ContinuousMultilinearMap.compContinuousLinearMapL (E := fun (x : ι) ↦ F) (E₁ := fun (x : ι) ↦ G)
            (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).2 ∘SL
          ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
            ((i : ι) → F →L[𝕜] G) :
        ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
          ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
      ((fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).1.fderivCompContinuousLinearMap (E := fun (x : ι) ↦ F)
            (E₁ := fun (x : ι) ↦ G) (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).2 ∘SL
          ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
            ((i : ι) → F →L[𝕜] G) :
        ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
          ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H))
    (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2)

Tactic:
have H₁ := ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap
    (fg.1.1, fun _ : ι ↦ fg.2)
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
F : Type u_4
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
inst_7 : Fintype ι
inst_8 : DecidableEq ι
fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)
H₁ :
  HasStrictFDerivAt
    (fun (fg : ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G)) ↦
      fg.1.compContinuousLinearMap (M₁ := fun (x : ι) ↦ F) (M₁' := fun (x : ι) ↦ G) fg.2)
    (HAdd.hAdd (α :=
      ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
        ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
      (β :=
      ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
        ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
      (ContinuousMultilinearMap.compContinuousLinearMapL (E := fun (x : ι) ↦ F) (E₁ := fun (x : ι) ↦ G)
            (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).2 ∘SL
          ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
            ((i : ι) → F →L[𝕜] G) :
        ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
          ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
      ((fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).1.fderivCompContinuousLinearMap (E := fun (x : ι) ↦ F)
            (E₁ := fun (x : ι) ↦ G) (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).2 ∘SL
          ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
            ((i : ι) → F →L[𝕜] G) :
        ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
          ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H))
    (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2)
⊢ HasStrictFDerivAt
    (⇑(toContinuousMultilinearMapCLM 𝕜) : (a : G [⋀^ι]→L[𝕜] H) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) H)
    (toContinuousMultilinearMapCLM 𝕜) fg.1

Tactic:
have H₂ := ((toContinuousMultilinearMapCLM 𝕜).hasStrictFDerivAt (x := fg.1))
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
F : Type u_4
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
inst_7 : Fintype ι
inst_8 : DecidableEq ι
fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)
H₁ :
  HasStrictFDerivAt
    (fun (fg : ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G)) ↦
      fg.1.compContinuousLinearMap (M₁ := fun (x : ι) ↦ F) (M₁' := fun (x : ι) ↦ G) fg.2)
    (HAdd.hAdd (α :=
      ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
        ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
      (β :=
      ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
        ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
      (ContinuousMultilinearMap.compContinuousLinearMapL (E := fun (x : ι) ↦ F) (E₁ := fun (x : ι) ↦ G)
            (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).2 ∘SL
          ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
            ((i : ι) → F →L[𝕜] G) :
        ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
          ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
      ((fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).1.fderivCompContinuousLinearMap (E := fun (x : ι) ↦ F)
            (E₁ := fun (x : ι) ↦ G) (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).2 ∘SL
          ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
            ((i : ι) → F →L[𝕜] G) :
        ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
          ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H))
    (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2)
H₂ :
  HasStrictFDerivAt
    (⇑(toContinuousMultilinearMapCLM 𝕜) : (a : G [⋀^ι]→L[𝕜] H) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) H)
    (toContinuousMultilinearMapCLM 𝕜) fg.1
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := (i : ι) → F →L[𝕜] G) (fun (x : F →L[𝕜] G) (i : ι) ↦ id x)
    (ContinuousLinearMap.pi (φ := fun (i : ι) ↦ F →L[𝕜] G) fun (i : ι) ↦ ContinuousLinearMap.id 𝕜 (F →L[𝕜] G)) fg.2

Tactic:
have H₃ := hasStrictFDerivAt_pi.mpr fun i : ι ↦ hasStrictFDerivAt_id (𝕜 := 𝕜) fg.2
-- 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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
g' : E →L[𝕜] F →L[𝕜] G
x : E
inst_9 : Fintype ι
inst_10 : DecidableEq ι
hf : HasStrictFDerivAt f f' x
hg : HasStrictFDerivAt g g' x
⊢ HasStrictFDerivAt (fun (x : E) ↦ (f x).compContinuousLinearMap (g x))
    (HAdd.hAdd (β := E →L[𝕜] F [⋀^ι]→L[𝕜] H) (compContinuousLinearMapCLM (g x) ∘SL f')
      ((f x).fderivCompContinuousLinearMap (g x) ∘SL g'))
    x

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

Premises used: ContinuousLinearMap.comp, HasStrictFDerivAt.prodMk, HasStrictFDerivAt.comp
-- 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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
g' : E →L[𝕜] F →L[𝕜] G
x : E
inst_9 : Fintype ι
inst_10 : DecidableEq ι
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
⊢ HasFDerivAt ((fun (fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)) ↦ fg.1.compContinuousLinearMap fg.2) ∘ fun (x : E) ↦ (f x, g x))
    (HAdd.hAdd (α := G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H) (β :=
        G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
        (compContinuousLinearMapCLM (f x, g x).2 ∘SL ContinuousLinearMap.fst 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
          G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
        ((f x, g x).1.fderivCompContinuousLinearMap (f x, g x).2 ∘SL
            ContinuousLinearMap.snd 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
          G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H) ∘SL
      f'.prod g')
    x

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

Premises used: HasFDerivAt.prodMk, HasFDerivAt.comp
-- 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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
g' : E →L[𝕜] F →L[𝕜] G
x : E
inst_9 : Fintype ι
inst_10 : DecidableEq ι
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
⊢ HasFDerivAt (fun (x : E) ↦ (f x).compContinuousLinearMap (g x))
    (HAdd.hAdd (β := E →L[𝕜] F [⋀^ι]→L[𝕜] H) (compContinuousLinearMapCLM (g x) ∘SL f')
      ((f x).fderivCompContinuousLinearMap (g x) ∘SL g'))
    x

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

Premises used: HasFDerivAt.prodMk, HasFDerivAt.comp
-- 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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
g' : E →L[𝕜] F →L[𝕜] G
s : Set E
x : E
inst_9 : Fintype ι
inst_10 : DecidableEq ι
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
⊢ HasFDerivWithinAt
    ((fun (fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)) ↦ fg.1.compContinuousLinearMap fg.2) ∘ fun (x : E) ↦ (f x, g x))
    (HAdd.hAdd (α := G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H) (β :=
        G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
        (compContinuousLinearMapCLM (f x, g x).2 ∘SL ContinuousLinearMap.fst 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
          G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
        ((f x, g x).1.fderivCompContinuousLinearMap (f x, g x).2 ∘SL
            ContinuousLinearMap.snd 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
          G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H) ∘SL
      f'.prod g')
    s x

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

Premises used: HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk
-- 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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
g' : E →L[𝕜] F →L[𝕜] G
s : Set E
x : E
inst_9 : Fintype ι
inst_10 : DecidableEq ι
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
⊢ HasFDerivWithinAt (fun (x : E) ↦ (f x).compContinuousLinearMap (g x))
    (HAdd.hAdd (β := E →L[𝕜] F [⋀^ι]→L[𝕜] H) (compContinuousLinearMapCLM (g x) ∘SL f')
      ((f x).fderivCompContinuousLinearMap (g x) ∘SL g'))
    s x

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

Premises used: HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk
-- 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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
s : Set E
x : E
inst_9 : Fintype ι
inst_10 : DecidableEq ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun (x : E) ↦ (f x).compContinuousLinearMap (g x)) s x =
    HAdd.hAdd (α := E →L[𝕜] F [⋀^ι]→L[𝕜] H) (compContinuousLinearMapCLM (g x) ∘SL fderivWithin 𝕜 f s x)
      ((f x).fderivCompContinuousLinearMap (g x) ∘SL fderivWithin 𝕜 g s x)

Tactic:
hf.hasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap (hg.hasFDerivWithinAt)
    |>.fderivWithin hs

Premises used: HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, 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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
x : E
inst_9 : Fintype ι
inst_10 : DecidableEq ι
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
⊢ fderiv 𝕜 (fun (x : E) ↦ (f x).compContinuousLinearMap (g x)) x =
    HAdd.hAdd (α := E →L[𝕜] F [⋀^ι]→L[𝕜] H) (compContinuousLinearMapCLM (g x) ∘SL fderiv 𝕜 f x)
      ((f x).fderivCompContinuousLinearMap (g x) ∘SL fderiv 𝕜 g x)

Tactic:
hf.hasFDerivAt.continuousAlternatingMapCompContinuousLinearMap (hg.hasFDerivAt) |>.fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap
-- 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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
s : Set E
x : E
inst_9 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
intro :
  ∀ (val : Fintype ι),
    DifferentiableWithinAt 𝕜 (F := F [⋀^ι]→L[𝕜] H) (fun (x : E) ↦ (f x).compContinuousLinearMap (g x)) s x
⊢ DifferentiableWithinAt 𝕜 (F := F [⋀^ι]→L[𝕜] H) (fun (x : E) ↦ (f x).compContinuousLinearMap (g 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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
s : Set E
x : E
inst_9 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
val : Fintype ι
⊢ DifferentiableWithinAt 𝕜 (F := F [⋀^ι]→L[𝕜] H) (fun (x : E) ↦ (f x).compContinuousLinearMap (g x)) s x

Tactic:
hf.hasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap hg.hasFDerivWithinAt
    |>.differentiableWithinAt

Premises used: HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, 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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
s : Set E
x : E
inst_9 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
val : Fintype ι
⊢ DifferentiableWithinAt 𝕜 (F := F [⋀^ι]→L[𝕜] H) (fun (x : E) ↦ (f x).compContinuousLinearMap (g x)) s x

Tactic:
exact hf.hasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap hg.hasFDerivWithinAt
    |>.differentiableWithinAt

Premises used: HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, 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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
s : Set E
x : E
inst_9 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
val : Fintype ι
⊢ DifferentiableWithinAt 𝕜 (F := F [⋀^ι]→L[𝕜] H) (fun (x : E) ↦ (f x).compContinuousLinearMap (g x)) s x

Tactic:
classical
  exact hf.hasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap hg.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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
x : E
inst_9 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
intro :
  ∀ (val : Fintype ι), DifferentiableAt 𝕜 (F := F [⋀^ι]→L[𝕜] H) (fun (x : E) ↦ (f x).compContinuousLinearMap (g x)) x
⊢ DifferentiableAt 𝕜 (F := F [⋀^ι]→L[𝕜] H) (fun (x : E) ↦ (f x).compContinuousLinearMap (g 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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
x : E
inst_9 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
val : Fintype ι
⊢ DifferentiableAt 𝕜 (F := F [⋀^ι]→L[𝕜] H) (fun (x : E) ↦ (f x).compContinuousLinearMap (g x)) x

Tactic:
hf.hasFDerivAt.continuousAlternatingMapCompContinuousLinearMap hg.hasFDerivAt
    |>.differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap
-- 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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
x : E
inst_9 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
val : Fintype ι
⊢ DifferentiableAt 𝕜 (F := F [⋀^ι]→L[𝕜] H) (fun (x : E) ↦ (f x).compContinuousLinearMap (g x)) x

Tactic:
exact hf.hasFDerivAt.continuousAlternatingMapCompContinuousLinearMap hg.hasFDerivAt
    |>.differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap
-- 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
H : Type u_6
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
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
x : E
inst_9 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
val : Fintype ι
⊢ DifferentiableAt 𝕜 (F := F [⋀^ι]→L[𝕜] H) (fun (x : E) ↦ (f x).compContinuousLinearMap (g x)) x

Tactic:
classical
  exact hf.hasFDerivAt.continuousAlternatingMapCompContinuousLinearMap hg.hasFDerivAt
    |>.differentiableAt