-- 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_1 : F → FormalMultilinearSeries 𝕜 F G
p_1 : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
m : Fin c.length
q q' : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F
H :
  ∀ (v : (i : Fin n) → E),
    Eq.{u_4 + 1} (α := G)
      (((fun
                  (p :
                    (i : Fin c.length) →
                      ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
                c.compAlongOrderedFinpartition f p)
              (update (β := fun (i : Fin c.length) ↦
                ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m (q + q')) :
            (a : (i : Fin n) → E) → G)
          v :
        G)
      ((HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)
              ((fun
                    (p :
                      (i : Fin c.length) →
                        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
                  c.compAlongOrderedFinpartition f p)
                (update (β := fun (i : Fin c.length) ↦
                  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q))
              ((fun
                    (p :
                      (i : Fin c.length) →
                        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
                  c.compAlongOrderedFinpartition f p)
                (update (β := fun (i : Fin c.length) ↦
                  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q')) :
            (a : (i : Fin n) → E) → G)
          v :
        G)
⊢ (fun (p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
        c.compAlongOrderedFinpartition f p)
      (update (β := fun (i : Fin c.length) ↦
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m (q + q')) =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)
      ((fun
            (p :
              (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
          c.compAlongOrderedFinpartition f p)
        (update (β := fun (i : Fin c.length) ↦
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q))
      ((fun
            (p :
              (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
          c.compAlongOrderedFinpartition f p)
        (update (β := fun (i : Fin c.length) ↦
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q'))

Tactic:
ext v