-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
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
h :
  ∀ (hij : i < c.index 0),
    (↑(if h : c.index 0 = c.index 0 then
              (c.emb (c.index 0)
                    (Fin.cast (n :=
                      update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          (c.index 0) +
                        1)
                      ⋯
                      (succ
                        (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                                (c.index 0) -
                              1,
                            ⋯⟩ :
                          Fin
                            (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0)
                              (c.partSize (c.index 0) - 1) (c.index 0)))))).pred
                ⋯
            else
              (c.emb (c.index 0)
                    (Fin.cast ⋯
                      (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                              (c.index 0) -
                            1,
                          ⋯⟩ :
                        Fin
                          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            (c.index 0))))).pred
                ⋯) :
          ℕ) +
        1 =
      (↑((fun (m : Fin c.length) ↦ c.emb m (⟨c.partSize m - 1, ⋯⟩ : Fin (c.partSize m))) (c.index 0)) : ℕ)
h₁ :
  ∀ (hj : j ≠ c.index 0),
    (↑(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
                ⋯) :
          ℕ) +
        1 =
      (↑((fun (m : Fin c.length) ↦ c.emb m (⟨c.partSize m - 1, ⋯⟩ : Fin (c.partSize m))) j) : ℕ)
⊢ (↑(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
              ⋯) :
        ℕ) +
      1 =
    (↑((fun (m : Fin c.length) ↦ c.emb m (⟨c.partSize m - 1, ⋯⟩ : Fin (c.partSize m))) j) : ℕ)

Tactic:
rcases eq_or_ne j (c.index 0) with rfl | hj

Premises used: OrderedFinpartition.index, eq_or_ne, OfNat.ofNat, rfl