-- 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
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
i : Fin c.length
h :
  ∀ (e : E) (v : (i : Fin m) → E),
    Eq.{u_4 + 1} (α := G)
      (((((q.compAlongOrderedFinpartition p (c.extend (some i))).curryLeft (Ei := fun (i : Fin (m + 1)) ↦ E) :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) G)
                e :
              ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :
            (a : (i : Fin m) → E) → G)
          v :
        G)
      ((((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)
                        ((compAlongOrderedFinpartitionL 𝕜 E F G c :
                            (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 c.length))
                        (fun (i : Fin c.length) ↦ p (c.partSize i)) 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 + 1)) ↦ E)
                        (p (c.partSize i + 1)) :
                      E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) G)
                e :
              ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :
            (a : (i : Fin m) → E) → G)
          v :
        G)
⊢ (q.compAlongOrderedFinpartition p (c.extend (some i))).curryLeft (Ei := fun (i : Fin (m + 1)) ↦ E) =
    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)
          ((compAlongOrderedFinpartitionL 𝕜 E F G c :
              (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 c.length))
          (fun (i : Fin c.length) ↦ p (c.partSize i)) 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 + 1)) ↦ E) (p (c.partSize i + 1)) :
        E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)

Tactic:
ext e v