-- 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
H₃ :
  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
⊢ 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

Tactic:
H₁.comp fg (H₂.prodMap fg H₃)

Premises used: ContinuousLinearMap.comp, ContinuousAlternatingMap.toContinuousMultilinearMapLinear, HasStrictFDerivAt.prodMap, HasStrictFDerivAt.comp, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousAlternatingMap.toContinuousMultilinearMapCLM