-- 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))
h₁ :
  ∀ (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)
⊢ Eq (α := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) 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)
    (∑ 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) :
      E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)

Tactic:
ext v