-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
hg : ContDiffWithinAt 𝕜 3 g t (f x)
hf : ContDiffWithinAt 𝕜 3 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
simp :
  HAdd.hAdd (α := F)
      ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → E) → F) fun (j : Fin 3) ↦
          iteratedDerivWithin
            (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j) f s
            x :
        F)
      (HAdd.hAdd (α := F)
        ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (j : Fin 2) ↦
            iteratedDerivWithin (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 2 (fun (x : Fin 1) ↦ 1) j) f s x :
          F)
        (HAdd.hAdd (α := F)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (j : Fin 2) ↦
              iteratedDerivWithin
                (update (β := fun (a : Fin 2) ↦ ℕ) (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) 1 2 j) f
                s x :
            F)
          (HAdd.hAdd (α := F) (β := F)
            ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (j : Fin 2) ↦
                iteratedDerivWithin
                  (update (β := fun (a : Fin 2) ↦ ℕ) (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) 1 2 j)
                  f s x :
              F)
            ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 3 f s x) : F)))) =
    HAdd.hAdd (α := F)
      ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦ derivWithin f s x : F)
      (HAdd.hAdd (α := F)
        ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
            ![iteratedDerivWithin 2 f s x, derivWithin f s x] :
          F)
        (HAdd.hAdd (α := F)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
              ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
            F)
          (HAdd.hAdd (α := F) (β := F)
            ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
                ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
              F)
            ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 3 f s x) : F))))
⊢ HAdd.hAdd (α := F)
        ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → E) → F) fun (j : Fin 3) ↦
            iteratedDerivWithin
              (OrderedFinpartition.partSize (n := 3)
                (OrderedFinpartition.extendLeft (OrderedFinpartition.extendLeft (OrderedFinpartition.atomic 1))) j)
              f s x :
          F)
        (HAdd.hAdd (α := F) (β := F)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (j : Fin 2) ↦
              iteratedDerivWithin
                (OrderedFinpartition.partSize (n := 3)
                  (OrderedFinpartition.extendMiddle (OrderedFinpartition.extendLeft (OrderedFinpartition.atomic 1)) 0)
                  j)
                f s x :
            F)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (j : Fin 2) ↦
              iteratedDerivWithin
                (OrderedFinpartition.partSize (n := 3)
                  (OrderedFinpartition.extendMiddle (OrderedFinpartition.extendLeft (OrderedFinpartition.atomic 1)) 1)
                  j)
                f s x :
            F)) +
      HAdd.hAdd (α := F) (β := F)
        ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (j : Fin 2) ↦
            iteratedDerivWithin
              (OrderedFinpartition.partSize (n := 3)
                (OrderedFinpartition.extendLeft
                  (OrderedFinpartition.extendMiddle (OrderedFinpartition.atomic 1) default))
                j)
              f s x :
          F)
        ((iteratedFDerivWithin 𝕜 1 g t (f x) : (a : (i : Fin 1) → E) → F) fun (j : Fin 1) ↦
            iteratedDerivWithin
              (OrderedFinpartition.partSize (n := 3)
                (OrderedFinpartition.extendMiddle
                  (OrderedFinpartition.extendMiddle (OrderedFinpartition.atomic 1) default) default)
                j)
              f s x :
          F) =
    HAdd.hAdd (β := F)
      (HAdd.hAdd (α := F) (β := F)
          ((iteratedFDerivWithin 𝕜 3 g t (f x) : (a : (i : Fin 3) → E) → F) fun (x_1 : Fin 3) ↦ derivWithin f s x : F)
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
              ![iteratedDerivWithin 2 f s x, derivWithin f s x] :
            F) +
        HSMul.hSMul (α := ℕ) (β := F) 2
          ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F)
              ![derivWithin f s x, iteratedDerivWithin 2 f s x] :
            F))
      ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 3 f s x) : F)

Tactic:
simp only [OrderedFinpartition.extendLeft_partSize, OrderedFinpartition.extendLeft_length,
      OrderedFinpartition.atomic_length, Nat.reduceAdd, OrderedFinpartition.atomic_partSize,
      Fin.isValue, OrderedFinpartition.extendMiddle_partSize, Fin.cons_zero, Fin.update_cons_zero,
      Fin.cons_one, Fin.default_eq_zero, OrderedFinpartition.extendMiddle_length, Fin.cons_update,
      Fin.succ_zero_eq_one, update_self, update_idem,
      iteratedFDerivWithin_one_apply (ht _ <| hst hx), add_assoc, two_smul]

Premises used: OrderedFinpartition.extendMiddle_length, add_assoc, OrderedFinpartition.atomic_length, two_smul, Nat.reduceAdd, iteratedFDerivWithin_one_apply, Fin.update_cons_zero, Fin.succ_zero_eq_one, Fin.cons_one, OrderedFinpartition.extendLeft_partSize, Fin.isValue, Function.update_idem, OrderedFinpartition.extendMiddle_partSize, OrderedFinpartition.extendLeft_length, Fin.default_eq_zero, Function.update_self, OrderedFinpartition.atomic_partSize, Fin.cons_update, Fin.cons_zero