-- 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
n_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
i : Fin c.length
length :
  OrderedFinpartition.length (n := n)
      { length := (c.extendMiddle i).length,
        partSize :=
          update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
            ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1),
        partSize_pos := ⋯,
        emb :=
          fun (i_1 : Fin (c.extendMiddle i).length)
            (j :
              Fin
                (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
                  ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) i_1)) ↦
          if h : i_1 = i then ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j.succ)).pred ⋯
          else ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j)).pred ⋯,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition n } =
    c.length
⊢ { length := (c.extendMiddle i).length,
      partSize :=
        update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
          ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1),
      partSize_pos := ⋯,
      emb :=
        fun (i_1 : Fin (c.extendMiddle i).length)
          (j :
            Fin
              (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
                ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) i_1)) ↦
        if h : i_1 = i then ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j.succ)).pred ⋯
        else ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j)).pred ⋯,
      emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ } =
    c
have partSize : HEq (α :=
  Fin
      (OrderedFinpartition.length (n := n)
        { length := (c.extendMiddle i).length,
          partSize :=
            update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
              ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1),
          partSize_pos := sorry,
          emb :=
            fun (i_1 : Fin (c.extendMiddle i).length)
              (j :
                Fin
                  (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
                    ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) i_1)) ↦
            if h : i_1 = i then ((c.extendMiddle i).emb i_1 (Fin.cast sorry j.succ)).pred sorry
            else ((c.extendMiddle i).emb i_1 (Fin.cast sorry j)).pred sorry,
          emb_strictMono := sorry, parts_strictMono := sorry, disjoint := sorry, cover := sorry }) →
    ℕ)
  (partSize
    { length := (c.extendMiddle i).length,
      partSize :=
        update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
          ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1),
      partSize_pos := sorry,
      emb :=
        fun (i_1 : Fin (c.extendMiddle i).length)
          (j :
            Fin
              (update (β := fun (a : Fin (c.extendMiddle i).length) ↦ ℕ) (c.extendMiddle i).partSize
                ((c.extendMiddle i).index 0) ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) i_1)) ↦
        if h : i_1 = i then ((c.extendMiddle i).emb i_1 (Fin.cast sorry j.succ)).pred sorry
        else ((c.extendMiddle i).emb i_1 (Fin.cast sorry j)).pred sorry,
      emb_strictMono := sorry, parts_strictMono := sorry, disjoint := sorry, cover := sorry })
  c.partSize
Tactic: ext