-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap (goal)
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
        (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
have 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)
Tactic: convert! this.comp fg hasStrictFDerivAt_snd |>.clm_apply hasStrictFDerivAt_fst