-- 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_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 :
  ∀ (a : Fin c.length),
    HEq (α :=
      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)
            a) →
        Fin (n + 1))
      (if h_1 : a = 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) a)) ↦
              if h : a = c.index 0 then (c.emb a (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb a (Fin.cast ⋯ j)).pred ⋯) ∘
            Fin.cast ⋯)
      (c.emb a)
⊢ ∀
    (a :
      Fin
        { 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)
    (a' : Fin c.length),
    a ≍ a' →
      { 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) }.emb
          a ≍
        c.emb a'

Tactic:
simp only [heq_eq_eq, forall_eq']

Premises used: heq_eq_eq, forall_eq'