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
hq :
  ∀ (n : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin n) ↦ F) G) (fun (x : F) ↦ q x n) t
hp :
  ∀ (n : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (fun (x : E) ↦ p x n) s
f : E → F
hf : AnalyticOn 𝕜 f s
h : MapsTo f s t
n : ℕ
c : OrderedFinpartition n
h_1 : Membership.mem (γ := Finset (OrderedFinpartition n)) 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 n) ↦ E) G) :=
  OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ AnalyticOn 𝕜 (F :=
    (m : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F)
    (fun (x : E) (m : Fin c.length) ↦ p x (c.partSize m)) s

Tactic:
exact AnalyticOn.pi (fun i ↦ hp _)

Premises used: AnalyticOn.pi
-- 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
e : E
v : (i : Fin m) → E
h :
  Eq.{u_3 + 1} (α := (i : Fin (c.length + 1)) → F)
    (fun (m_1 : Fin (c.length + 1)) ↦
      (p (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m_1) :
          (a : (i : Fin (cons 1 c.partSize m_1)) → E) → F)
        (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
          (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (m + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m_2 : Fin c.length) ↦ succ ∘ c.emb m_2) m_1)))
    (cons (α := fun (i : Fin (c.length + 1)) ↦ F)
      ((p 1 : (a : (i : Fin 1) → E) → F) (snoc (α := fun (i : Fin 1) ↦ E) ![] e)) fun (m_1 : Fin c.length) ↦
      (p (c.partSize m_1) : (a : (i : Fin (c.partSize m_1)) → E) → F) (v ∘ c.emb m_1))
⊢ Eq.{u_4 + 1} (α := G)
    ((q (c.length + 1) : (a : (i : Fin (c.length + 1)) → F) → G) fun (m_1 : Fin (c.length + 1)) ↦
        (p (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m_1) :
            (a : (i : Fin (cons 1 c.partSize m_1)) → E) → F)
          (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
            (cases (motive := fun (x : Fin (c.length + 1)) ↦
              Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (m + 1))
              (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
              (fun (m_2 : Fin c.length) ↦ succ ∘ c.emb m_2) m_1)) :
      G)
    ((q (c.length + 1) : (a : (i : Fin (c.length + 1)) → F) → G)
        (cons (α := fun (i : Fin (c.length + 1)) ↦ F)
          ((p 1 : (a : (i : Fin 1) → E) → F) (snoc (α := fun (i : Fin 1) ↦ E) ![] e)) fun (m_1 : Fin c.length) ↦
          (p (c.partSize m_1) : (a : (i : Fin (c.partSize m_1)) → E) → F) (v ∘ c.emb m_1)) :
      G)

Tactic:
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
e : E
v : (i : Fin m) → E
h :
  ∀ (j : Fin (c.length + 1)),
    Eq.{u_3 + 1} (α := F)
      ((p (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize j) : (a : (i : Fin (cons 1 c.partSize j)) → E) → F)
          (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
            (cases (motive := fun (x : Fin (c.length + 1)) ↦
              Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (m + 1))
              (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
              (fun (m_1 : Fin c.length) ↦ succ ∘ c.emb m_1) j)) :
        F)
      (cons (α := fun (i : Fin (c.length + 1)) ↦ F)
          ((p 1 : (a : (i : Fin 1) → E) → F) (snoc (α := fun (i : Fin 1) ↦ E) ![] e))
          (fun (m_1 : Fin c.length) ↦ (p (c.partSize m_1) : (a : (i : Fin (c.partSize m_1)) → E) → F) (v ∘ c.emb m_1))
          j :
        F)
⊢ Eq.{u_3 + 1} (α := (i : Fin (c.length + 1)) → F)
    (fun (m_1 : Fin (c.length + 1)) ↦
      (p (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize m_1) :
          (a : (i : Fin (cons 1 c.partSize m_1)) → E) → F)
        (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
          (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (m + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m_2 : Fin c.length) ↦ succ ∘ c.emb m_2) m_1)))
    (cons (α := fun (i : Fin (c.length + 1)) ↦ F)
      ((p 1 : (a : (i : Fin 1) → E) → F) (snoc (α := fun (i : Fin 1) ↦ E) ![] e)) fun (m_1 : Fin c.length) ↦
      (p (c.partSize m_1) : (a : (i : Fin (c.partSize m_1)) → E) → F) (v ∘ c.emb m_1))

Tactic:
ext j
-- 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
e : E
v : (i : Fin m) → E
j : Fin (c.length + 1)
⊢ Eq.{u_3 + 1} (α := F)
    ((p (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize j) : (a : (i : Fin (cons 1 c.partSize j)) → E) → F)
        (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
          (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (m + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m_1 : Fin c.length) ↦ succ ∘ c.emb m_1) j)) :
      F)
    (cons (α := fun (i : Fin (c.length + 1)) ↦ F)
        ((p 1 : (a : (i : Fin 1) → E) → F) (snoc (α := fun (i : Fin 1) ↦ E) ![] e))
        (fun (m_1 : Fin c.length) ↦ (p (c.partSize m_1) : (a : (i : Fin (c.partSize m_1)) → E) → F) (v ∘ c.emb m_1)) j :
      F)

Tactic:
Fin.cases rfl (fun i ↦ rfl) j

Premises used: Fin.cases
-- 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
e : E
v : (i : Fin m) → E
j : Fin (c.length + 1)
⊢ Eq.{u_3 + 1} (α := F)
    ((p (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize j) : (a : (i : Fin (cons 1 c.partSize j)) → E) → F)
        (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
          (cases (motive := fun (x : Fin (c.length + 1)) ↦
            Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize x) → Fin (m + 1))
            (fun (x : Fin (cons (α := fun (a : Fin (c.length + 1)) ↦ ℕ) 1 c.partSize 0)) ↦ 0)
            (fun (m_1 : Fin c.length) ↦ succ ∘ c.emb m_1) j)) :
      F)
    (cons (α := fun (i : Fin (c.length + 1)) ↦ F)
        ((p 1 : (a : (i : Fin 1) → E) → F) (snoc (α := fun (i : Fin 1) ↦ E) ![] e))
        (fun (m_1 : Fin c.length) ↦ (p (c.partSize m_1) : (a : (i : Fin (c.partSize m_1)) → E) → F) (v ∘ c.emb m_1)) j :
      F)

Tactic:
exact Fin.cases rfl (fun i ↦ rfl) j
-- 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
h :
  Eq.{u_3 + 1} (α := (i : Fin c.length) → F)
    (fun (m_1 : Fin c.length) ↦
      (p (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize i (c.partSize i + 1) m_1) :
          (a : (i : Fin (update c.partSize i (c.partSize i + 1) m_1)) → E) → F)
        (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
          (if h : m_1 = 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 m_1 ∘ Fin.cast ⋯)))
    fun (m_1 : Fin c.length) ↦
    ((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)
            m_1 :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m_1)) ↦ E) F) :
        (a : (i : Fin (c.partSize m_1)) → E) → F)
      (v ∘ c.emb m_1)
⊢ Eq.{u_4 + 1} (α := G)
    ((q c.length : (a : (i : Fin c.length) → F) → G) fun (m_1 : Fin c.length) ↦
        (p (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize i (c.partSize i + 1) m_1) :
            (a : (i : Fin (update c.partSize i (c.partSize i + 1) m_1)) → E) → F)
          (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
            (if h : m_1 = 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 m_1 ∘ Fin.cast ⋯)) :
      G)
    ((q c.length : (a : (i : Fin c.length) → F) → G) fun (m_1 : Fin c.length) ↦
        ((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)
                m_1 :
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m_1)) ↦ E) F) :
            (a : (i : Fin (c.partSize m_1)) → E) → F)
          (v ∘ c.emb m_1) :
      G)

Tactic:
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
h :
  ∀ (j : Fin c.length),
    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)
⊢ Eq.{u_3 + 1} (α := (i : Fin c.length) → F)
    (fun (m_1 : Fin c.length) ↦
      (p (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize i (c.partSize i + 1) m_1) :
          (a : (i : Fin (update c.partSize i (c.partSize i + 1) m_1)) → E) → F)
        (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
          (if h : m_1 = 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 m_1 ∘ Fin.cast ⋯)))
    fun (m_1 : Fin c.length) ↦
    ((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)
            m_1 :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m_1)) ↦ E) F) :
        (a : (i : Fin (c.partSize m_1)) → E) → F)
      (v ∘ c.emb m_1)

Tactic:
ext j
-- 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
e : E
v : (i : Fin m) → E
j : Fin c.length
h :
  Eq.{u_3 + 1} (α := F)
    ((p (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j) :
          (a : (i : Fin (update c.partSize j (c.partSize j + 1) j)) → E) → F)
        (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
          ((fun (i : Fin (c.partSize j + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (m + 1)) 0 (succ ∘ c.emb j) i) ∘
            Fin.cast ⋯)) :
      F)
    ((p (c.partSize j + 1) : (a : (i : Fin (c.partSize j + 1)) → E) → F)
        (cons (α := fun (i : Fin (c.partSize j + 1)) ↦ E) e (v ∘ c.emb j)) :
      F)
⊢ Eq.{u_3 + 1} (α := F)
    ((p (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j) :
          (a : (i : Fin (update c.partSize j (c.partSize j + 1) j)) → E) → F)
        (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
          (if h : j = j then
            (fun (i : Fin (c.partSize j + 1)) ↦
                cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (m + 1)) 0 (succ ∘ c.emb j) i) ∘
              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)) j
              ((ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (c.partSize j + 1)) ↦ E) (p (c.partSize j + 1)) :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize j)) ↦ 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 [↓reduceDIte, update_self, ContinuousMultilinearMap.curryLeft_apply,
      Nat.succ_eq_add_one]

Premises used: Nat.succ_eq_add_one, reduceDIte, ContinuousMultilinearMap.curryLeft_apply, Function.update_self
-- 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
e : E
v : (i : Fin m) → E
j : Fin c.length
⊢ update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j = c.partSize j + 1

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
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : (i : Fin m) → E
j : Fin c.length
h :
  ∀ (i : ℕ) (him : i < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j)
    (hin : i < c.partSize j + 1),
    Eq.{u_2 + 1} (α := E)
      (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
          ((fun (i : Fin (c.partSize j + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (m + 1)) 0 (succ ∘ c.emb j) i) ∘
            Fin.cast ⋯)
          (⟨i, him⟩ : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j)) :
        E)
      (cons (α := fun (i : Fin (c.partSize j + 1)) ↦ E) e (v ∘ c.emb j) (⟨i, hin⟩ : Fin (c.partSize j + 1)) : E)
⊢ Eq.{u_3 + 1} (α := F)
    ((p (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j) :
          (a : (i : Fin (update c.partSize j (c.partSize j + 1) j)) → E) → F)
        (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
          ((fun (i : Fin (c.partSize j + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (m + 1)) 0 (succ ∘ c.emb j) i) ∘
            Fin.cast ⋯)) :
      F)
    ((p (c.partSize j + 1) : (a : (i : Fin (c.partSize j + 1)) → E) → F)
        (cons (α := fun (i : Fin (c.partSize j + 1)) ↦ E) e (v ∘ c.emb j)) :
      F)

Tactic:
apply FormalMultilinearSeries.congr _ (by simp)

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
e : E
v : (i : Fin m) → E
j : Fin c.length
a : ℕ
ha : 0 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j
h'a : 0 < c.partSize j + 1
⊢ Eq.{u_2 + 1} (α := E)
    (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
        ((fun (i : Fin (c.partSize j + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (m + 1)) 0 (succ ∘ c.emb j) i) ∘
          Fin.cast ⋯)
        (⟨0, ha⟩ : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j)) :
      E)
    (cons (α := fun (i : Fin (c.partSize j + 1)) ↦ E) e (v ∘ c.emb j) (⟨0, h'a⟩ : Fin (c.partSize j + 1)) : E)

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
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : (i : Fin m) → E
j : Fin c.length
a_1 a : ℕ
ha : a + 1 < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j
h'a : a + 1 < c.partSize j + 1
⊢ Eq.{u_2 + 1} (α := E)
    (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
        ((fun (i : Fin (c.partSize j + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (m + 1)) 0 (succ ∘ c.emb j) i) ∘
          Fin.cast ⋯)
        (⟨a + 1, ha⟩ : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j)) :
      E)
    (cons (α := fun (i : Fin (c.partSize j + 1)) ↦ E) e (v ∘ c.emb j) (⟨a + 1, h'a⟩ : Fin (c.partSize j + 1)) : E)

Tactic:
simp [cons]

Premises used: Fin.cons
-- 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
e : E
v : (i : Fin m) → E
j : Fin c.length
a : ℕ
ha : a < update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j
h'a : a < c.partSize j + 1
⊢ Eq.{u_2 + 1} (α := E)
    (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
        ((fun (i : Fin (c.partSize j + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (m + 1)) 0 (succ ∘ c.emb j) i) ∘
          Fin.cast ⋯)
        (⟨a, ha⟩ : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j)) :
      E)
    (cons (α := fun (i : Fin (c.partSize j + 1)) ↦ E) e (v ∘ c.emb j) (⟨a, h'a⟩ : Fin (c.partSize j + 1)) : E)

Tactic:
match a with
    | 0 => simp
    | a + 1 => simp [cons]