-- 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
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
i : Fin c.length
e : E
v : (i : Fin m) → E
j : Fin c.length
h :
  Eq.{u_3 + 1} (α := F)
    ((p (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j) :
          (a : (i : Fin (update c.partSize j (c.partSize j + 1) j)) → E) → F)
        (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
          (if h : j = j then
            (fun (i : Fin (c.partSize j + 1)) ↦
                cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (m + 1)) 0 (succ ∘ c.emb j) i) ∘
              Fin.cast ⋯
          else succ ∘ c.emb j ∘ Fin.cast ⋯)) :
      F)
    (((update (β := fun (i : Fin c.length) ↦
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
              (fun (i : Fin c.length) ↦ p (c.partSize i)) j
              ((ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (c.partSize j + 1)) ↦ E) (p (c.partSize j + 1)) :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize j)) ↦ E) F)
                e)
              j :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize j)) ↦ E) F) :
          (a : (i : Fin (c.partSize j)) → E) → F)
        (v ∘ c.emb j) :
      F)
h₁ :
  ∀ (hij : j ≠ i),
    Eq.{u_3 + 1} (α := F)
      ((p (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize i (c.partSize i + 1) j) :
            (a : (i : Fin (update c.partSize i (c.partSize i + 1) j)) → E) → F)
          (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
            (if h : j = i then
              (fun (i_1 : Fin (c.partSize i + 1)) ↦
                  cases (motive := fun (x : Fin (c.partSize i + 1)) ↦ Fin (m + 1)) 0 (succ ∘ c.emb i) i_1) ∘
                Fin.cast ⋯
            else succ ∘ c.emb j ∘ Fin.cast ⋯)) :
        F)
      (((update (β := fun (i : Fin c.length) ↦
                ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                (fun (i : Fin c.length) ↦ p (c.partSize i)) i
                ((ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (c.partSize i + 1)) ↦ E)
                      (p (c.partSize i + 1)) :
                    (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                  e)
                j :
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize j)) ↦ E) F) :
            (a : (i : Fin (c.partSize j)) → E) → F)
          (v ∘ c.emb j) :
        F)
⊢ Eq.{u_3 + 1} (α := F)
    ((p (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize i (c.partSize i + 1) j) :
          (a : (i : Fin (update c.partSize i (c.partSize i + 1) j)) → E) → F)
        (comp (β := Fin (m + 1)) (cons (α := fun (i : Fin (m + 1)) ↦ E) e v)
          (if h : j = i then
            (fun (i_1 : Fin (c.partSize i + 1)) ↦
                cases (motive := fun (x : Fin (c.partSize i + 1)) ↦ Fin (m + 1)) 0 (succ ∘ c.emb i) i_1) ∘
              Fin.cast ⋯
          else succ ∘ c.emb j ∘ Fin.cast ⋯)) :
      F)
    (((update (β := fun (i : Fin c.length) ↦
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
              (fun (i : Fin c.length) ↦ p (c.partSize i)) i
              ((ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin (c.partSize i + 1)) ↦ E) (p (c.partSize i + 1)) :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                e)
              j :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize j)) ↦ E) F) :
          (a : (i : Fin (c.partSize j)) → E) → F)
        (v ∘ c.emb j) :
      F)

Tactic:
rcases eq_or_ne j i with rfl | hij

Premises used: eq_or_ne, rfl