awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
e : E
v : (i : Fin m) → E
j : Fin c.length
hij : j ≠ i
h :
  Eq.{u_3 + 1} (α := F)
    ((p (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize i (c.partSize i + 1) j) :
          (a : (i : Fin (update c.partSize i (c.partSize i + 1) j)) → E) → F)
        (cons (α := fun (i : Fin (m + 1)) ↦ E) e v ∘ succ ∘ c.emb j ∘ Fin.cast ⋯) :
      F)
    ((p (c.partSize j) : (a : (i : Fin (c.partSize j)) → E) → F) (v ∘ c.emb j) : F)
⊢ Eq.{u_3 + 1} (α := F)
    ((p (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize i (c.partSize i + 1) j) :
          (a : (i : Fin (update c.partSize i (c.partSize i + 1) j)) → E) → F)
        (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
          (if h : j = i then
            (fun (i_1 : Fin (c.partSize i + 1)) ↦
                cases (motive := fun (x : Fin (c.partSize i + 1)) ↦ Fin (m + 1)) 0 (succ ∘ c.emb i) i_1) ∘
              Fin.cast ⋯
          else succ ∘ c.emb j ∘ Fin.cast ⋯)) :
      F)
    (((update (β := fun (i : Fin c.length) ↦
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
              (fun (i : Fin c.length) ↦ p (c.partSize i)) i
              ((ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (c.partSize i + 1)) ↦ E) (p (c.partSize i + 1)) :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                e)
              j :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize j)) ↦ E) F) :
          (a : (i : Fin (c.partSize j)) → E) → F)
        (v ∘ c.emb j) :
      F)

Tactic:
simp only [hij, ↓reduceDIte, ne_eq, not_false_eq_true, update_of_ne]

Premises used: reduceDIte, ne_eq, not_false_eq_true, Function.update_of_ne
-- 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
e : E
v : (i : Fin m) → E
j : Fin c.length
hij : j ≠ i
⊢ update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize i (c.partSize i + 1) j = c.partSize j

Tactic:
simp [hij]
-- 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
e : E
v : (i : Fin m) → E
j : Fin c.length
hij : j ≠ i
h :
  ∀ (i_1 : ℕ) (him : i_1 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize i (c.partSize i + 1) j)
    (hin : i_1 < c.partSize j),
    (cons (α := fun (i : Fin (m + 1)) ↦ E) e v ∘ succ ∘ c.emb j ∘ Fin.cast ⋯) ⟨i_1, him⟩ =
      (v ∘ c.emb j) (⟨i_1, hin⟩ : Fin (c.partSize j))
⊢ Eq.{u_3 + 1} (α := F)
    ((p (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize i (c.partSize i + 1) j) :
          (a : (i : Fin (update c.partSize i (c.partSize i + 1) j)) → E) → F)
        (cons (α := fun (i : Fin (m + 1)) ↦ E) e v ∘ succ ∘ c.emb j ∘ Fin.cast ⋯) :
      F)
    ((p (c.partSize j) : (a : (i : Fin (c.partSize j)) → E) → F) (v ∘ c.emb j) : F)

Tactic:
apply FormalMultilinearSeries.congr _ (by simp [hij])

Premises used: FormalMultilinearSeries.congr
-- 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
e : E
v : (i : Fin m) → E
j : Fin c.length
hij : j ≠ i
⊢ ∀ (i_1 : ℕ) (him : i_1 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize i (c.partSize i + 1) j)
    (hin : i_1 < c.partSize j),
    (cons (α := fun (i : Fin (m + 1)) ↦ E) e v ∘ succ ∘ c.emb j ∘ Fin.cast ⋯) ⟨i_1, him⟩ =
      (v ∘ c.emb j) (⟨i_1, hin⟩ : Fin (c.partSize j))

Tactic:
simp
-- 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
zero_eq : ∀ x ∈ s, ContinuousMultilinearMap.curry0 ((q (f x)).taylorComp (p x) 0) = (g ∘ f) x
fderivWithin :
  ∀ (m : ℕ),
    (↑m : WithTop ℕ∞) < n →
      ∀ x ∈ s,
        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)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) ((q (f x)).taylorComp (p x) m.succ)) s x
cont :
  ∀ (m : ℕ),
    (↑m : WithTop ℕ∞) ≤ n →
      ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
        (fun (x : E) ↦ (q (f x)).taylorComp (p x) m) s
⊢ HasFTaylorSeriesUpToOn.{u_1, u_2, u_4} (𝕜 := 𝕜) n (g ∘ f) (fun (x : E) ↦ (q (f x)).taylorComp (p x)) s

Tactic:
constructor
-- 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
x : E
hx : x ∈ s
⊢ ContinuousMultilinearMap.curry0 ((q (f x)).taylorComp (p x) 0) = (g ∘ f) x

Tactic:
simp [FormalMultilinearSeries.taylorComp, default, HasFTaylorSeriesUpToOn.zero_eq' hg (h hx)]

Premises used: Inhabited.default, HasFTaylorSeriesUpToOn.zero_eq', FormalMultilinearSeries.taylorComp
-- 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
c : OrderedFinpartition m
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
change :
  HasFDerivWithinAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
    (fun (y : E) ↦
      (((B :
                (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 (f y) c.length) :
            ContinuousMultilinearMap 𝕜
              (fun (i : Fin c.length) ↦
                ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
              (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)) :
          (a : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) G)
        fun (i : Fin c.length) ↦ p y (c.partSize i))
    (∑ i : Option (Fin c.length),
      ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft (Ei := fun (i : Fin (m + 1)) ↦ E))
    s x
⊢ 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

Tactic:
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

Premises used: Finset.univ, FormalMultilinearSeries.compAlongOrderedFinpartition, HasFDerivWithinAt, ContinuousMultilinearMap.curryLeft, OrderedFinpartition.extend, OrderedFinpartition.partSize, DFunLike.coe, Finset.sum, OrderedFinpartition.length
-- 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
c : OrderedFinpartition m
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ LE.le (α := WithTop ℕ∞) (↑c.length : WithTop ℕ∞) (↑m : WithTop ℕ∞)

Tactic:
have cm : (c.length : WithTop ℕ∞) ≤ m := mod_cast OrderedFinpartition.length_le c
-- 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
c : OrderedFinpartition m
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : LE.le (α := WithTop ℕ∞) (↑c.length : WithTop ℕ∞) (↑m : WithTop ℕ∞)
i : Fin c.length
⊢ LE.le (α := WithTop ℕ∞) (↑(c.partSize i) : WithTop ℕ∞) (↑m : WithTop ℕ∞)

Tactic:
exact_mod_cast OrderedFinpartition.partSize_le c i

Premises used: OrderedFinpartition.partSize_le
-- 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
c : OrderedFinpartition m
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : LE.le (α := WithTop ℕ∞) (↑c.length : WithTop ℕ∞) (↑m : WithTop ℕ∞)
⊢ ∀ (i : Fin c.length), LE.le (α := WithTop ℕ∞) (↑(c.partSize i) : WithTop ℕ∞) (↑m : WithTop ℕ∞)

Tactic:
have cp i : (c.partSize i : WithTop ℕ∞) ≤ m := by
        exact_mod_cast OrderedFinpartition.partSize_le c i
-- 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
c : OrderedFinpartition m
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : LE.le (α := WithTop ℕ∞) (↑c.length : WithTop ℕ∞) (↑m : WithTop ℕ∞)
cp : ∀ (i : Fin c.length), LE.le (α := WithTop ℕ∞) (↑(c.partSize i) : WithTop ℕ∞) (↑m : WithTop ℕ∞)
⊢ ∀ (i : Fin c.length),
    HasFDerivWithinAt (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
      (fun (x : E) ↦ p x (c.partSize i))
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (c.partSize i).succ) ↦ E) (p x (c.partSize i).succ)) s x

Tactic:
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
-- 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
c : OrderedFinpartition m
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : LE.le (α := WithTop ℕ∞) (↑c.length : WithTop ℕ∞) (↑m : WithTop ℕ∞)
cp : ∀ (i : Fin c.length), LE.le (α := WithTop ℕ∞) (↑(c.partSize i) : WithTop ℕ∞) (↑m : WithTop ℕ∞)
I :
  ∀ (i : Fin c.length),
    HasFDerivWithinAt (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
      (fun (x : E) ↦ p x (c.partSize i))
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (c.partSize i).succ) ↦ E) (p x (c.partSize i).succ)) s x
⊢ HasFDerivWithinAt (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G)
    (fun (x : F) ↦ q x c.length)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin c.length.succ) ↦ F) (q (f x) c.length.succ)) t (f x)

Tactic:
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)
-- 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
c : OrderedFinpartition m
B : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜
    (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : LE.le (α := WithTop ℕ∞) (↑c.length : WithTop ℕ∞) (↑m : WithTop ℕ∞)
cp : ∀ (i : Fin c.length), LE.le (α := WithTop ℕ∞) (↑(c.partSize i) : WithTop ℕ∞) (↑m : WithTop ℕ∞)
I :
  ∀ (i : Fin c.length),
    HasFDerivWithinAt (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
      (fun (x : E) ↦ p x (c.partSize i))
      (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (c.partSize i).succ) ↦ E) (p x (c.partSize i).succ)) s x
J :
  HasFDerivWithinAt (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G)
    (fun (x : F) ↦ q x c.length)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin c.length.succ) ↦ F) (q (f x) c.length.succ)) t (f x)
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p x 1))
    s x

Tactic:
have K : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x :=
        hf.hasFDerivWithinAt hm.ne_bot hx
-- 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
⊢ ∀ (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

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 hm.ne_bot 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]
-- 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
⊢ 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

Tactic:
have 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 :=
      HasFDerivWithinAt.fun_sum (fun c _ ↦ A c)