-- 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
e_4 :
  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
e_5 :
  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))))
e_6 :
  Eq (α :=
    TopologicalSpace
      (ContinuousMultilinearMap 𝕜 G H ×
        ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))))
    instTopologicalSpaceProd UniformSpace.toTopologicalSpace
e_8 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap 𝕜 F H)) (instAddCommGroup (M₁ := F)) NormedAddCommGroup.toAddCommGroup
e_9 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap 𝕜 F H)) (instModule (M₁ := F)) (β :=
    Module 𝕜 (ContinuousMultilinearMap 𝕜 F H)) NormedSpace.toModule
e_10 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap 𝕜 F H)) (instTopologicalSpace (E := F))
    UniformSpace.toTopologicalSpace
x : ContinuousMultilinearMap 𝕜 G H
x_1 : (i : ι) → F i
⊢ Eq.{u_6 + 1} (α := 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))) ∘SL
                  ContinuousLinearMap.inl 𝕜 (ContinuousMultilinearMap 𝕜 G H)
                    ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) :
                (a : ContinuousMultilinearMap 𝕜 G H) → ContinuousMultilinearMap 𝕜 F H)
              x :
            ContinuousMultilinearMap 𝕜 F H) :
          (a : (i : ι) → F i) → H)
        x_1 :
      H)
    ((((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ :=
                  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)
                  (ContinuousLinearMap.inl 𝕜 (ContinuousMultilinearMap 𝕜 G H)
                    ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))) :
                (a : ContinuousMultilinearMap 𝕜 G H) → ContinuousMultilinearMap 𝕜 F H)
              x :
            ContinuousMultilinearMap 𝕜 F H) :
          (a : (i : ι) → F i) → H)
        x_1 :
      H)

Tactic:
simp [fderivCompContinuousLinearMap]

Premises used: ContinuousMultilinearMap.fderivCompContinuousLinearMap