-- 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 : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i j : Fin c.length
hij : i < j
⊢ (↑(if h : i = c.index 0 then
          (c.emb i
                (Fin.cast ⋯
                  (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i - 1,
                        ⋯⟩ :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          i)).succ)).pred
            ⋯
        else
          (c.emb i
                (Fin.cast ⋯
                  (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i - 1,
                      ⋯⟩ :
                    Fin
                      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        i)))).pred
            ⋯) :
      ℕ) <
    (↑(if h : j = c.index 0 then
          (c.emb j
                (Fin.cast ⋯
                  (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j - 1,
                        ⋯⟩ :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          j)).succ)).pred
            ⋯
        else
          (c.emb j
                (Fin.cast ⋯
                  (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j - 1,
                      ⋯⟩ :
                    Fin
                      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        j)))).pred
            ⋯) :
      ℕ)
have rw : (↑(if h : i = c.index 0 then
          (c.emb i
                (Fin.cast sorry
                  (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i - 1,
                        sorry⟩ :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          i)).succ)).pred
            sorry
        else
          (c.emb i
                (Fin.cast sorry
                  (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i - 1,
                      sorry⟩ :
                    Fin
                      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        i)))).pred
            sorry) :
      ℕ) +
    1 <
  (↑(if h : j = c.index 0 then
          (c.emb j
                (Fin.cast sorry
                  (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j - 1,
                        sorry⟩ :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          j)).succ)).pred
            sorry
        else
          (c.emb j
                (Fin.cast sorry
                  (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j - 1,
                      sorry⟩ :
                    Fin
                      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        j)))).pred
            sorry) :
      ℕ) +
    1
Tactic: rw [← Nat.add_lt_add_iff_right (k := 1)]