-- 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)
j : Fin (c.partSize (c.index 0))
neg :
  c.emb (c.index 0) 0 =
    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 ⋯)
      (Fin.cast ⋯
        (⟨(↑0 : ℕ), ⋯⟩ :
          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)
              (c.index 0))))
⊢ c.emb (c.index 0) j =
    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 ⋯)
      (Fin.cast ⋯
        (⟨(↑j : ℕ), ⋯⟩ :
          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)
              (c.index 0))))
have neg₁ : ∀ (hj : j ≠ 0),
  c.emb (c.index 0) j =
    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)
      (Fin.cast sorry
        (⟨(↑j : ℕ), sorry⟩ :
          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)
              (c.index 0))))
Tactic: rcases eq_or_ne j 0 with rfl | hj