-- 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))
this :
  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
h :
  Eq (α :=
      AddCommGroup
        (ContinuousMultilinearMap 𝕜 G H ×
          ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))))
      Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup →
    HEq (α :=
        Module 𝕜
          (ContinuousMultilinearMap 𝕜 G H ×
            ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))))
        Prod.instModule (β :=
        Module 𝕜
          (ContinuousMultilinearMap 𝕜 G H ×
            ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))))
        (NormedSpace.toModule :
          Module 𝕜
            (ContinuousMultilinearMap 𝕜 G H ×
              ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)))) →
      Eq (α :=
          TopologicalSpace
            (ContinuousMultilinearMap 𝕜 G H ×
              ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))))
          instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
        Eq (α := AddCommGroup (ContinuousMultilinearMap 𝕜 F H)) (instAddCommGroup (M₁ := F))
            NormedAddCommGroup.toAddCommGroup →
          HEq (α := Module 𝕜 (ContinuousMultilinearMap 𝕜 F H)) (instModule (M₁ := F)) (β :=
              Module 𝕜 (ContinuousMultilinearMap 𝕜 F H)) NormedSpace.toModule →
            Eq (α := TopologicalSpace (ContinuousMultilinearMap 𝕜 F H)) (instTopologicalSpace (E := F))
                UniformSpace.toTopologicalSpace →
              Eq (α :=
                ContinuousMultilinearMap 𝕜 G H ×
                    ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) →L[𝕜]
                  ContinuousMultilinearMap 𝕜 F H)
                (fg.1.fderivCompContinuousLinearMap (E := F) (E₁ := G) fg.2 ∘SL
                  ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H)
                    ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)))
                ((ContinuousLinearMap.flip
                      (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 ∘SL
                        ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H)
                          ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))) :
                    (a : ContinuousMultilinearMap 𝕜 G H) →
                      ContinuousMultilinearMap 𝕜 G H × ((i : ι) → F i →L[𝕜] G i) →L[𝕜] ContinuousMultilinearMap 𝕜 F H)
                  fg.1)
⊢ HasStrictFDerivAt
    (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)
    (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) fg.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)
      (fg.1.fderivCompContinuousLinearMap (E := F) (E₁ := G) fg.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))
    fg

Tactic:
convert! this.comp fg hasStrictFDerivAt_snd |>.clm_apply hasStrictFDerivAt_fst

Premises used: hasStrictFDerivAt_snd, hasStrictFDerivAt_fst, HasStrictFDerivAt.clm_apply, HasStrictFDerivAt.comp