-- 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.compAlongOrderedFinpartition p (c.extend none)).curryLeft (Ei := fun (i : Fin (m + 1)) ↦ E) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) G)
              e :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :
          (a : (i : Fin m) → E) → G)
        v :
      G)
    ((((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ :=
                  ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G)
                  ((ContinuousLinearMap.flipMultilinear (E := fun (i : Fin c.length) ↦
                        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                        (compAlongOrderedFinpartitionL 𝕜 E F G c) :
                      (a : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) →
                        ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
                          ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) G)
                    fun (i : Fin c.length) ↦ p (c.partSize i))
                  (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
                    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (c.length + 1)) ↦ F) (q (c.length + 1)))
                    ((continuousMultilinearCurryFin1 𝕜 E F :
                        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
                      (p 1))) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E) G)
              e :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G) :
          (a : (i : Fin m) → E) → G)
        v :
      G)
have h : 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: simp only [Nat.succ_eq_add_one, OrderedFinpartition.extend, extendLeft,
    ContinuousMultilinearMap.curryLeft_apply,
    FormalMultilinearSeries.compAlongOrderedFinpartition_apply, applyOrderedFinpartition_apply,
    ContinuousLinearMap.coe_comp', comp_apply, continuousMultilinearCurryFin1_apply,
    Matrix.zero_empty, ContinuousLinearMap.flipMultilinear_apply_apply,
    compAlongOrderedFinpartitionL_apply, compAlongOrderFinpartition_apply]