awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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 := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)
    ((fun
          (p :
            ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G ×
              ((m : Fin c.length) →
                ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ 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 n) ↦ 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 n) ↦ E) G)) :
            (a : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) →
              ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) G)
          p.2) ∘
      fun (x : E) ↦ (q (f x) c.length, fun (m : Fin c.length) ↦ p x (c.partSize m)))
    s
have apply : AnalyticOn 𝕜 (F :=
  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))
  (fun (x : E) ↦ (q (f x) c.length, fun (m : Fin c.length) ↦ p x (c.partSize m))) s
Tactic: apply B.analyticOnNhd_uncurry_of_multilinear.comp_analyticOn ?_ (mapsTo_univ _ _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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 :=
    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))
    (fun (x : E) ↦ (q (f x) c.length, fun (m : Fin c.length) ↦ p x (c.partSize m))) s
have hf₁ : AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G)
  (fun (x : E) ↦ q (f x) c.length) s
Tactic: apply AnalyticOn.prod
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
hf₁ :
  AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G)
    (fun (x : E) ↦ q (f x) c.length) s
⊢ AnalyticOn 𝕜 (F :=
    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))
    (fun (x : E) ↦ (q (f x) c.length, fun (m : Fin c.length) ↦ p x (c.partSize m))) s
have hg : 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: apply AnalyticOn.prod
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ 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)
have 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))
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ 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))
have 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)
Tactic: ext j
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ 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)
have 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 sorry
        else succ ∘ c.emb m_1 ∘ Fin.cast sorry)))
  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: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ 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)
have 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 sorry
          else succ ∘ c.emb j ∘ Fin.cast sorry)) :
      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: ext j
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ 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)
have 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)
        (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 sorry
        else succ ∘ c.emb j ∘ Fin.cast sorry)) :
    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: rcases eq_or_ne j i with rfl | hij
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ 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)
have 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 sorry)) :
    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: simp only [↓reduceDIte, update_self, ContinuousMultilinearMap.curryLeft_apply,
      Nat.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ 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)
have 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 sorry)
        (⟨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)
Tactic: apply FormalMultilinearSeries.congr _ (by simp)