-- 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}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
i : Fin c.length
neg :
  c.partSize i =
    update (β := fun (a : Fin c.length) ↦ ℕ)
      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)) (c.index 0)
      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) + 1) i
⊢ HEq (α :=
    Fin
        (update (β := fun (a : Fin c.length) ↦ ℕ)
          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)) (c.index 0)
          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) + 1)
          i) →
      Fin (n + 1))
    (if h_1 : i = c.index 0 then
      (fun
            (i :
              Fin
                (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                    (c.index 0) +
                  1)) ↦
          cases (motive :=
            fun
              (x :
                Fin
                  (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                      (c.index 0) +
                    1)) ↦
            Fin (n + 1)) 0
            (succ ∘
              fun
                (j :
                  Fin
                    (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                      (c.index 0))) ↦
              (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯)
            i) ∘
        Fin.cast ⋯
    else
      succ ∘
        (fun
              (j :
                Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
            if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯) ∘
          Fin.cast ⋯)
    (c.emb i)
have neg₁ : ∀ (i_1 : Fin (c.partSize i)),
  c.emb i i_1 =
    (if h_1 : i = c.index 0 then
        (fun
              (i :
                Fin
                  (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                      (c.index 0) +
                    1)) ↦
            cases (motive :=
              fun
                (x :
                  Fin
                    (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        (c.index 0) +
                      1)) ↦
              Fin (n + 1)) 0
              (succ ∘
                fun
                  (j :
                    Fin
                      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        (c.index 0))) ↦
                (c.emb (c.index 0) (Fin.cast sorry j.succ)).pred sorry)
              i) ∘
          Fin.cast sorry
      else
        succ ∘
          (fun
                (j :
                  Fin
                    (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
              if h : i = c.index 0 then (c.emb i (Fin.cast sorry j.succ)).pred sorry else (c.emb i (Fin.cast sorry j)).pred sorry) ∘
            Fin.cast sorry)
      ⟨(↑i_1 : ℕ), sorry⟩
Tactic: refine ((Fin.heq_fun_iff ?_).mpr ?_).symm