-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
theorem HasFTaylorSeriesUpToOn.comp {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) :
    HasFTaylorSeriesUpToOn n (g ∘ f) (fun x ↦ (q (f x)).taylorComp (p x)) s

Proof state:
case fderivWithin
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : 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 < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x => (q (f x)).taylorComp (p x) m) ((q (f x)).taylorComp (p x) m.succ).curryLeft s x

Tactic:
have A (c : OrderedFinpartition m) :
  HasFDerivWithinAt (fun x ↦ (q (f x)).compAlongOrderedFinpartition (p x) c)
    (∑ i : Option (Fin c.length),
      ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x := by
  let B := c.compAlongOrderedFinpartitionL 𝕜 E F G
  change HasFDerivWithinAt (fun y ↦ B (q (f y) c.length) (fun i ↦ p y (c.partSize i)))
    (∑ i : Option (Fin c.length),
      ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
  have cm : (c.length : WithTop ℕ∞) ≤ m := mod_cast OrderedFinpartition.length_le c
  have cp i : (c.partSize i : WithTop ℕ∞) ≤ m := by
    exact_mod_cast OrderedFinpartition.partSize_le c i
  have I i : HasFDerivWithinAt (fun x ↦ p x (c.partSize i))
      (p x (c.partSize i).succ).curryLeft s x :=
    hf.fderivWithin (c.partSize i) ((cp i).trans_lt hm) x hx
  have J : HasFDerivWithinAt (fun x ↦ q x c.length) (q (f x) c.length.succ).curryLeft
    t (f x) := hg.fderivWithin c.length (cm.trans_lt hm) (f x) (h hx)
  have K : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x :=
    hf.hasFDerivWithinAt (le_trans (mod_cast Nat.le_add_left 1 m)
      (ENat.add_one_natCast_le_withTop_of_lt hm)) hx
  convert HasFDerivWithinAt.linear_multilinear_comp (J.comp x K h) I B
  simp only [B, Nat.succ_eq_add_one, Fintype.sum_option, comp_apply, faaDiBruno_aux1,
    faaDiBruno_aux2]

Result:
case fderivWithin
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : 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 < n
x : E
hx : x ∈ s
A :
  ∀ (c : OrderedFinpartition m),
    HasFDerivWithinAt (fun x => (q (f x)).compAlongOrderedFinpartition (p x) c)
      (∑ i : Option (Fin c.length), ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
⊢ HasFDerivWithinAt (fun x => (q (f x)).taylorComp (p x) m) ((q (f x)).taylorComp (p x) m.succ).curryLeft s x

Proof state:
case h.e'_12.h.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : 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 < n
x : E
hx : x ∈ s
A :
  ∀ (c : OrderedFinpartition m),
    HasFDerivWithinAt (fun x => (q (f x)).compAlongOrderedFinpartition (p x) c)
      (∑ i : Option (Fin c.length), ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
B :
  HasFDerivWithinAt (fun x => (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)
    s x
this :
  ∑ 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✝ : Fin m → E
⊢ ((∑ c : OrderedFinpartition m,
            ∑ i : Option (Fin c.length), (q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft
        v)
      x✝ =
    ((∑ c : OrderedFinpartition m,
          ∑ i : Option (Fin c.length), ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft)
        v)
      x✝

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]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : 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 < n
x : E
hx : x ∈ s
c : OrderedFinpartition m
B : ContinuousMultilinearMap 𝕜 (fun i => F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : ↑c.length ≤ ↑m
cp : ∀ (i : Fin c.length), ↑(c.partSize i) ≤ ↑m
I : ∀ (i : Fin c.length), HasFDerivWithinAt (fun x => p x (c.partSize i)) (p x (c.partSize i).succ).curryLeft s x
J : HasFDerivWithinAt (fun x => q x c.length) (q (f x) c.length.succ).curryLeft t (f x)
⊢ HasFDerivWithinAt (fun y => (B (q (f y) c.length)) fun i => p y (c.partSize i))
    (∑ i : Option (Fin c.length), ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x

Tactic:
have K : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x :=
  hf.hasFDerivWithinAt (le_trans (mod_cast Nat.le_add_left 1 m)
    (ENat.add_one_natCast_le_withTop_of_lt hm)) hx

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : 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 < n
x : E
hx : x ∈ s
c : OrderedFinpartition m
B : ContinuousMultilinearMap 𝕜 (fun i => F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : ↑c.length ≤ ↑m
cp : ∀ (i : Fin c.length), ↑(c.partSize i) ≤ ↑m
I : ∀ (i : Fin c.length), HasFDerivWithinAt (fun x => p x (c.partSize i)) (p x (c.partSize i).succ).curryLeft s x
J : HasFDerivWithinAt (fun x => q x c.length) (q (f x) c.length.succ).curryLeft t (f x)
K : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x
⊢ HasFDerivWithinAt (fun y => (B (q (f y) c.length)) fun i => p y (c.partSize i))
    (∑ i : Option (Fin c.length), ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x