-- 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
h :
  ∀ (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)
h₁ :
  ∀ (x : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) (x_1 : (i : ι) → F i),
    Eq.{u_6 + 1} (α := H)
      ((((ContinuousLinearMap.comp (M₂ :=
                    ContinuousMultilinearMap 𝕜 G H ×
                      ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)))
                    (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.inr 𝕜 (ContinuousMultilinearMap 𝕜 G H)
                      ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))) :
                  (a : (i : ι) → F i →L[𝕜] G i) → 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.inr 𝕜 (ContinuousMultilinearMap 𝕜 G H)
                      ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))) :
                  (a : (i : ι) → F i →L[𝕜] G i) → ContinuousMultilinearMap 𝕜 F H)
                x :
              ContinuousMultilinearMap 𝕜 F H) :
            (a : (i : ι) → F i) → H)
          x_1 :
        H)
⊢ 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:
ext