-- 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)
neg :
  { length := c.length,
        partSize :=
          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),
        partSize_pos := ⋯,
        emb := fun (m : Fin c.length) ↦
          if h_1 : m = 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)
                          m)) ↦
                  if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯) ∘
                Fin.cast ⋯,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) }.length =
    c.length
neg₁ :
  { length := c.length,
        partSize :=
          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),
        partSize_pos := ⋯,
        emb := fun (m : Fin c.length) ↦
          if h_1 : m = 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)
                          m)) ↦
                  if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯) ∘
                Fin.cast ⋯,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) }.partSize ≍
    c.partSize
⊢ { length := c.length,
      partSize :=
        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),
      partSize_pos := ⋯,
      emb := fun (m : Fin c.length) ↦
        if h_1 : m = 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)
                        m)) ↦
                if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯) ∘
              Fin.cast ⋯,
      emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ : OrderedFinpartition (n + 1) } =
    c
have neg₂ : { length := c.length,
      partSize :=
        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),
      partSize_pos := sorry,
      emb := fun (m : Fin c.length) ↦
        if h_1 : m = 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)
                        m)) ↦
                if h : m = c.index 0 then (c.emb m (Fin.cast sorry j.succ)).pred sorry else (c.emb m (Fin.cast sorry j)).pred sorry) ∘
              Fin.cast sorry,
      emb_strictMono := sorry, parts_strictMono := sorry, disjoint := sorry, cover := sorry : OrderedFinpartition (n + 1) }.emb ≍
  c.emb
Tactic: ext