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
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))
rw :
  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.{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)))
    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)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) ((q (f x)).taylorComp (p x) m.succ)) s x

Tactic:
rw [← this]
-- 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))
⊢ 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:
B
-- 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₁ :
  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)
⊢ 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.{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)))
    s x

Tactic:
convert! B
-- 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
fderivWithin :
  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))
⊢ 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

Tactic:
suffices ∑ 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) by
      rw [← this]
      convert! B
      ext v
      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]
-- 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
fderivWithin :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin (m + 1)) ↦ E) G)
    (∑
      x_1 ∈
        Finset.sigma (α := fun (a : OrderedFinpartition m) ↦ Option (Fin a.length)) Finset.univ
          fun (c : OrderedFinpartition m) ↦ Finset.univ,
      (q (f x)).compAlongOrderedFinpartition (p x)
        (x_1.fst (β := fun (i : OrderedFinpartition m) ↦ Option (Fin i.length)).extend
          (x_1.snd (β := fun (i : OrderedFinpartition m) ↦ Option (Fin i.length)))))
    ((q (f x)).taylorComp (p x) (m + 1))
⊢ 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))

Tactic:
rw [Finset.sum_sigma']

Premises used: Finset.sum_sigma'
-- 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
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin (m + 1)) ↦ E) G)
    (∑
      x_1 ∈
        Finset.sigma (α := fun (a : OrderedFinpartition m) ↦ Option (Fin a.length)) Finset.univ
          fun (c : OrderedFinpartition m) ↦ Finset.univ,
      (q (f x)).compAlongOrderedFinpartition (p x)
        (x_1.fst (β := fun (i : OrderedFinpartition m) ↦ Option (Fin i.length)).extend
          (x_1.snd (β := fun (i : OrderedFinpartition m) ↦ Option (Fin i.length)))))
    ((q (f x)).taylorComp (p x) (m + 1))

Tactic:
Fintype.sum_equiv (OrderedFinpartition.extendEquiv m) _ _ (fun p ↦ rfl)

Premises used: Finset.univ, FormalMultilinearSeries.taylorComp, Finset.sigma, OrderedFinpartition.extendEquiv, Fintype.sum_equiv, rfl
-- 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
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin (m + 1)) ↦ E) G)
    (∑
      x_1 ∈
        Finset.sigma (α := fun (a : OrderedFinpartition m) ↦ Option (Fin a.length)) Finset.univ
          fun (c : OrderedFinpartition m) ↦ Finset.univ,
      (q (f x)).compAlongOrderedFinpartition (p x)
        (x_1.fst (β := fun (i : OrderedFinpartition m) ↦ Option (Fin i.length)).extend
          (x_1.snd (β := fun (i : OrderedFinpartition m) ↦ Option (Fin i.length)))))
    ((q (f x)).taylorComp (p x) (m + 1))

Tactic:
exact Fintype.sum_equiv (OrderedFinpartition.extendEquiv m) _ _ (fun p ↦ rfl)

Premises used: OrderedFinpartition.extendEquiv, Fintype.sum_equiv, rfl
-- 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
apply :
  ∀ (c : OrderedFinpartition m),
    Membership.mem (γ := Finset (OrderedFinpartition m)) Finset.univ c →
      ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
        (fun (a : E) ↦ (q (f a)).compAlongOrderedFinpartition (p a) c) s
⊢ 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

Tactic:
apply continuousOn_finsetSum _ (fun c _ ↦ ?_)

Premises used: continuousOn_finsetSum
-- 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
c : OrderedFinpartition m
h_1 : Membership.mem (γ := Finset (OrderedFinpartition m)) Finset.univ c
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 :
  ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
    ((fun
          (p :
            ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G ×
              ((i : Fin c.length) →
                ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)) ↦
        (((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))
                p.1 :
              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)
          p.2) ∘
      fun (x : E) ↦ (q (f x) c.length, fun (i : Fin c.length) ↦ p x (c.partSize i)))
    s
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
    (fun (a : E) ↦ (q (f a)).compAlongOrderedFinpartition (p a) c) s

Tactic:
change ContinuousOn
      ((fun p ↦ B p.1 p.2) ∘ (fun x ↦ (q (f x) c.length, fun i ↦ p x (c.partSize i)))) s

Premises used: Function.comp, Prod.mk, OrderedFinpartition.partSize, ContinuousOn, DFunLike.coe, 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
c : OrderedFinpartition m
h_1 : Membership.mem (γ := Finset (OrderedFinpartition m)) Finset.univ c
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
apply :
  ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G)
    (fun (x : E) ↦ q (f x) c.length) s
apply₁ :
  ContinuousOn (Y :=
    (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
    (fun (x : E) (i : Fin c.length) ↦ p x (c.partSize i)) s
⊢ ContinuousOn (Y := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
    ((fun
          (p :
            ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G ×
              ((i : Fin c.length) →
                ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)) ↦
        (((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))
                p.1 :
              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)
          p.2) ∘
      fun (x : E) ↦ (q (f x) c.length, fun (i : Fin c.length) ↦ p x (c.partSize i)))
    s

Tactic:
apply B.continuous_uncurry_of_multilinear.comp_continuousOn (ContinuousOn.prodMk ?_ ?_)

Premises used: Continuous.comp_continuousOn, ContinuousLinearMap.continuous_uncurry_of_multilinear, ContinuousOn.prodMk
-- 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
c : OrderedFinpartition m
h_1 : Membership.mem (γ := Finset (OrderedFinpartition m)) Finset.univ c
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 : (c.length : WithTop ℕ∞) ≤ m := mod_cast OrderedFinpartition.length_le c