-- 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 + 1)
h : range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
⊢ HEq (α :=
    (m :
        Fin
          (length (n := n + 1)
            { length := c.length - 1 + 1,
              partSize :=
                cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 fun (i : Fin (c.length - 1)) ↦
                  c.partSize (Fin.cast ⋯ i.succ),
              partSize_pos := ⋯,
              emb := fun (i : Fin (c.length - 1 + 1)) ↦
                cases (motive := fun (x : Fin (c.length - 1 + 1)) ↦
                  Fin
                      (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                        (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) x) →
                    Fin (n + 1))
                  (fun
                      (x :
                        Fin
                          (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                            (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) 0)) ↦
                    0)
                  (fun (m : Fin (c.length - 1)) ↦
                    succ ∘ fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯)
                  i,
              emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ })) →
      Fin
          (partSize
            { length := c.length - 1 + 1,
              partSize :=
                cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 fun (i : Fin (c.length - 1)) ↦
                  c.partSize (Fin.cast ⋯ i.succ),
              partSize_pos := ⋯,
              emb := fun (i : Fin (c.length - 1 + 1)) ↦
                cases (motive := fun (x : Fin (c.length - 1 + 1)) ↦
                  Fin
                      (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                        (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) x) →
                    Fin (n + 1))
                  (fun
                      (x :
                        Fin
                          (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                            (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) 0)) ↦
                    0)
                  (fun (m : Fin (c.length - 1)) ↦
                    succ ∘ fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯)
                  i,
              emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }
            m) →
        Fin (n + 1))
    (emb
      { length := c.length - 1 + 1,
        partSize :=
          cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 fun (i : Fin (c.length - 1)) ↦
            c.partSize (Fin.cast ⋯ i.succ),
        partSize_pos := ⋯,
        emb := fun (i : Fin (c.length - 1 + 1)) ↦
          cases (motive := fun (x : Fin (c.length - 1 + 1)) ↦
            Fin
                (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                  (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) x) →
              Fin (n + 1))
            (fun
                (x :
                  Fin
                    (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                      (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast ⋯ i.succ)) 0)) ↦
              0)
            (fun (m : Fin (c.length - 1)) ↦
              succ ∘ fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯)
            i,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ })
    c.emb
have pos : ∀
  (a :
    Fin
      (length (n := n + 1)
        { length := c.length - 1 + 1,
          partSize :=
            cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 fun (i : Fin (c.length - 1)) ↦
              c.partSize (Fin.cast sorry i.succ),
          partSize_pos := sorry,
          emb := fun (i : Fin (c.length - 1 + 1)) ↦
            cases (motive := fun (x : Fin (c.length - 1 + 1)) ↦
              Fin
                  (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                    (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast sorry i.succ)) x) →
                Fin (n + 1))
              (fun
                  (x :
                    Fin
                      (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                        (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast sorry i.succ)) 0)) ↦
                0)
              (fun (m : Fin (c.length - 1)) ↦
                succ ∘ fun (j : Fin (c.partSize (Fin.cast sorry m.succ))) ↦ (c.emb (Fin.cast sorry m.succ) j).pred sorry)
              i,
          emb_strictMono := sorry, parts_strictMono := sorry, disjoint := sorry, cover := sorry }))
  (a' : Fin c.length),
  a ≍ a' →
    emb
        { length := c.length - 1 + 1,
          partSize :=
            cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1 fun (i : Fin (c.length - 1)) ↦
              c.partSize (Fin.cast sorry i.succ),
          partSize_pos := sorry,
          emb := fun (i : Fin (c.length - 1 + 1)) ↦
            cases (motive := fun (x : Fin (c.length - 1 + 1)) ↦
              Fin
                  (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                    (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast sorry i.succ)) x) →
                Fin (n + 1))
              (fun
                  (x :
                    Fin
                      (cons (α := fun (a : Fin (c.length - 1 + 1)) ↦ ℕ) 1
                        (fun (i : Fin (c.length - 1)) ↦ c.partSize (Fin.cast sorry i.succ)) 0)) ↦
                0)
              (fun (m : Fin (c.length - 1)) ↦
                succ ∘ fun (j : Fin (c.partSize (Fin.cast sorry m.succ))) ↦ (c.emb (Fin.cast sorry m.succ) j).pred sorry)
              i,
          emb_strictMono := sorry, parts_strictMono := sorry, disjoint := sorry, cover := sorry : OrderedFinpartition (n + 1) }
        a ≍
      c.emb a'
Tactic: refine hfunext (congrArg Fin A) ?_