-- 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
n_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
i : Fin c.length
emb :
  ∀ (a : Fin c.length)
    (a' :
      Fin
        (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 := ⋯ })),
    a ≍ a' →
      c.emb a ≍
        OrderedFinpartition.emb
          { 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 }
          a'
⊢ HEq (α :=
    (m :
        Fin
          (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 := ⋯ })) →
      Fin
          (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 := ⋯,
              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 := ⋯ }
            m) →
        Fin n)
    (OrderedFinpartition.emb
      { 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.emb

Tactic:
refine HEq.symm (hfunext rfl ?_)

Premises used: HEq.symm, Function.hfunext, rfl