-- 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
⊢ HasStrictFDerivAt
    (fun
        (y :
          ContinuousMultilinearMap 𝕜 G H ×
            ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))) ↦
      (((compContinuousLinearMapContinuousMultilinear 𝕜 F G H :
                (a : (i : ι) → F i →L[𝕜] G i) → ContinuousMultilinearMap 𝕜 G H →L[𝕜] ContinuousMultilinearMap 𝕜 F H)
              y.2 :
            ContinuousMultilinearMap 𝕜 G H →L[𝕜] ContinuousMultilinearMap 𝕜 F H) :
          (a : ContinuousMultilinearMap 𝕜 G H) → ContinuousMultilinearMap 𝕜 F H)
        y.1)
    (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)
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((compContinuousLinearMapContinuousMultilinear 𝕜 F G H :
            (a : (i : ι) → F i →L[𝕜] G i) → ContinuousMultilinearMap 𝕜 G H →L[𝕜] ContinuousMultilinearMap 𝕜 F H)
          fg.2)
        (ContinuousLinearMap.fst 𝕜 (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 :
        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:
this.comp fg hasStrictFDerivAt_snd |>.clm_apply hasStrictFDerivAt_fst

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