-- 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
A :
  ∀ (c : OrderedFinpartition m),
    HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
      (fun (x : E) ↦ (q (f x)).compAlongOrderedFinpartition (p x) c)
      (∑ i : Option (Fin c.length),
        ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft (Ei := fun (i : Fin (m + 1)) ↦ E))
      s x
B :
  HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
    (fun (x : E) ↦ (q (f x)).taylorComp (p x) m)
    (∑ c : OrderedFinpartition m,
      ∑ i : Option (Fin c.length),
        ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft (Ei := fun (i : Fin (m + 1)) ↦ E))
    s x
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin (m + 1)) ↦ E) G)
    (∑ c : OrderedFinpartition m,
      ∑ i : Option (Fin c.length), (q (f x)).compAlongOrderedFinpartition (p x) (c.extend i))
    ((q (f x)).taylorComp (p x) (m + 1))
v : E
x_1 : (i : Fin m) → E
⊢ Eq.{u_4 + 1} (α := G)
    (((((ContinuousMultilinearMap.curryLeft.{u_1, u_2, u_4} (𝕜 := 𝕜) (Ei := fun (i : Fin m.succ) ↦ E) (G := G)
                    (∑ c : OrderedFinpartition m,
                      ∑ i : Option (Fin c.length), (q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)) :
                  E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) G)
              v :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :
          (a : (i : Fin m) → E) → G)
        x_1 :
      G)
    ((((∑ c : OrderedFinpartition m,
                  ∑ i : Option (Fin c.length),
                    ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft (Ei := fun (i : Fin (m + 1)) ↦
                      E) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) G)
              v :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :
          (a : (i : Fin m) → E) → G)
        x_1 :
      G)

Tactic:
simp only [Nat.succ_eq_add_one, Fintype.sum_option, ContinuousMultilinearMap.curryLeft_apply,
        ContinuousMultilinearMap.sum_apply, ContinuousMultilinearMap.add_apply,
        FormalMultilinearSeries.compAlongOrderedFinpartition_apply, ContinuousLinearMap.coe_sum',
        Finset.sum_apply, ContinuousLinearMap.add_apply]

Premises used: Nat.succ_eq_add_one, Fintype.sum_option, Finset.sum_apply, ContinuousMultilinearMap.sum_apply, ContinuousLinearMap.add_apply, ContinuousMultilinearMap.add_apply, ContinuousLinearMap.coe_sum', ContinuousMultilinearMap.curryLeft_apply, FormalMultilinearSeries.compAlongOrderedFinpartition_apply