-- 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_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)
⊢ Eq.{u_4 + 1} (α := G)
    (((((q.compAlongOrderedFinpartition p (c.extend (some i))).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_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                  (ContinuousMultilinearMap.toContinuousLinearMap (R := 𝕜) (M₁ := fun (i : Fin c.length) ↦
                      ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) (M₂ :=
                      ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
                      ((compAlongOrderedFinpartitionL 𝕜 E F G c :
                          (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 c.length))
                      (fun (i : Fin c.length) ↦ p (c.partSize i)) i :
                    ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F →L[𝕜]
                      ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
                  (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (c.partSize i + 1)) ↦ E)
                      (p (c.partSize i + 1)) :
                    E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) :
                (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)

Tactic:
simp only [OrderedFinpartition.extend, extendMiddle, ContinuousMultilinearMap.curryLeft_apply,
      Nat.succ_eq_add_one, FormalMultilinearSeries.compAlongOrderedFinpartition_apply,
      applyOrderedFinpartition_apply, ContinuousLinearMap.coe_comp', comp_apply,
      ContinuousMultilinearMap.toContinuousLinearMap_apply, compAlongOrderedFinpartitionL_apply,
      compAlongOrderFinpartition_apply]

Premises used: ContinuousLinearMap.coe_comp', Nat.succ_eq_add_one, ContinuousMultilinearMap.toContinuousLinearMap_apply, OrderedFinpartition.compAlongOrderedFinpartitionL_apply, OrderedFinpartition.compAlongOrderFinpartition_apply, OrderedFinpartition.applyOrderedFinpartition_apply, OrderedFinpartition.extend, OrderedFinpartition.extendMiddle, ContinuousMultilinearMap.curryLeft_apply, Function.comp_apply, FormalMultilinearSeries.compAlongOrderedFinpartition_apply