-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : (↑m : WithTop ℕ∞) < n
x : E
hx : x ∈ s
c : OrderedFinpartition m
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : LE.le (α := WithTop ℕ∞) (↑c.length : WithTop ℕ∞) (↑m : WithTop ℕ∞)
cp : ∀ (i : Fin c.length), LE.le (α := WithTop ℕ∞) (↑(c.partSize i) : WithTop ℕ∞) (↑m : WithTop ℕ∞)
I :
  ∀ (i : Fin c.length),
    HasFDerivWithinAt (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
      (fun (x : E) ↦ p x (c.partSize i))
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (c.partSize i).succ) ↦ E) (p x (c.partSize i).succ)) s x
J :
  HasFDerivWithinAt (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G)
    (fun (x : F) ↦ q x c.length)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin c.length.succ) ↦ F) (q (f x) c.length.succ)) t (f x)
K :
  HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p x 1))
    s x
h₁ :
  Eq (α := AddCommGroup (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G))
      (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin m) ↦ E)) NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G))
        (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin m) ↦ E)) (β :=
        Module 𝕜 (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)) NormedSpace.toModule →
      Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G))
          (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin m) ↦ E)) UniformSpace.toTopologicalSpace →
        ∑ i : Option (Fin c.length),
            ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft (Ei := fun (i : Fin (m + 1)) ↦ E) =
          HAdd.hAdd (α := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
            (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ :=
              ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G)
              ((B.flipMultilinear (E := fun (i : Fin c.length) ↦
                    ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) :
                  (a : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) →
                    ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
                      ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) G)
                fun (i : Fin c.length) ↦ p x (c.partSize i))
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
                (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin c.length.succ) ↦ F) (q (f x) c.length.succ))
                ((continuousMultilinearCurryFin1 𝕜 E F :
                    (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
                  (p x 1))))
            (∑ i : Fin c.length,
              ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ :=
                ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                (ContinuousMultilinearMap.toContinuousLinearMap (R := 𝕜) (M₁ := fun (i : Fin c.length) ↦
                    ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) (M₂ :=
                    ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
                    ((B :
                        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) ↦ F) G) →
                          ContinuousMultilinearMap 𝕜
                            (fun (i : Fin c.length) ↦ ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                            (ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) G))
                      (((fun (x : F) ↦ q x c.length) ∘ f) x))
                    (fun (j : Fin c.length) ↦ p x (c.partSize j)) i :
                  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F →L[𝕜]
                    ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
                (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (c.partSize i).succ) ↦ E)
                    (p x (c.partSize i).succ) :
                  E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F))
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
    (fun (y : E) ↦
      (((B :
                (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) ↦ F) G) →
                  ContinuousMultilinearMap 𝕜
                    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                    (ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) G))
              (q (f y) c.length) :
            ContinuousMultilinearMap 𝕜
              (fun (i : Fin c.length) ↦
                ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
              (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)) :
          (a : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) G)
        fun (i : Fin c.length) ↦ p y (c.partSize i))
    (∑ i : Option (Fin c.length),
      ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft (Ei := fun (i : Fin (m + 1)) ↦ E))
    s x

Tactic:
convert! HasFDerivWithinAt.linear_multilinear_comp (J.comp x K h) I B

Premises used: HasFDerivWithinAt.linear_multilinear_comp, HasFDerivWithinAt.comp