-- 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 𝕜 2 g t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
simp :
  HAdd.hAdd (α := F) (β := F)
      ((iteratedFDerivWithin 𝕜
              (OrderedFinpartition.length (n := 2)
                ((OrderedFinpartition.extendEquiv 1 :
                    (a : (c : OrderedFinpartition 1) × Option (Fin c.length)) → OrderedFinpartition (1 + 1))
                  (Sigma.mk (β := fun (c : OrderedFinpartition 1) ↦ Option (Fin c.length))
                    (OrderedFinpartition.atomic 1) none)))
              g t (f x) :
            (a :
                (i :
                    Fin
                      ((OrderedFinpartition.extendEquiv 1 :
                            (a : (c : OrderedFinpartition 1) × Option (Fin c.length)) → OrderedFinpartition (1 + 1))
                          ⟨OrderedFinpartition.atomic 1, none⟩).length) →
                  E) →
              F)
          fun
            (j :
              Fin
                (OrderedFinpartition.length (n := 2)
                  ((OrderedFinpartition.extendEquiv 1 :
                      (a : (c : OrderedFinpartition 1) × Option (Fin c.length)) → OrderedFinpartition (1 + 1))
                    (Sigma.mk (β := fun (c : OrderedFinpartition 1) ↦ Option (Fin c.length))
                      (OrderedFinpartition.atomic 1) none)))) ↦
          iteratedDerivWithin
            (OrderedFinpartition.partSize
              ((OrderedFinpartition.extendEquiv 1 :
                  (a : (c : OrderedFinpartition 1) × Option (Fin c.length)) → OrderedFinpartition (1 + 1))
                (Sigma.mk (β := fun (c : OrderedFinpartition 1) ↦ Option (Fin c.length)) (OrderedFinpartition.atomic 1)
                  none))
              j)
            f s x :
        F)
      ((iteratedFDerivWithin 𝕜
              (OrderedFinpartition.length (n := 2)
                ((OrderedFinpartition.extendEquiv 1 :
                    (a : (c : OrderedFinpartition 1) × Option (Fin c.length)) → OrderedFinpartition (1 + 1))
                  (Sigma.mk (β := fun (c : OrderedFinpartition 1) ↦ Option (Fin c.length))
                    (OrderedFinpartition.atomic 1) (some default))))
              g t (f x) :
            (a :
                (i :
                    Fin
                      ((OrderedFinpartition.extendEquiv 1 :
                            (a : (c : OrderedFinpartition 1) × Option (Fin c.length)) → OrderedFinpartition (1 + 1))
                          ⟨OrderedFinpartition.atomic 1, some default⟩).length) →
                  E) →
              F)
          fun
            (j :
              Fin
                (OrderedFinpartition.length (n := 2)
                  ((OrderedFinpartition.extendEquiv 1 :
                      (a : (c : OrderedFinpartition 1) × Option (Fin c.length)) → OrderedFinpartition (1 + 1))
                    (Sigma.mk (β := fun (c : OrderedFinpartition 1) ↦ Option (Fin c.length))
                      (OrderedFinpartition.atomic 1) (some default))))) ↦
          iteratedDerivWithin
            (OrderedFinpartition.partSize
              ((OrderedFinpartition.extendEquiv 1 :
                  (a : (c : OrderedFinpartition 1) × Option (Fin c.length)) → OrderedFinpartition (1 + 1))
                (Sigma.mk (β := fun (c : OrderedFinpartition 1) ↦ Option (Fin c.length)) (OrderedFinpartition.atomic 1)
                  (some default)))
              j)
            f s x :
        F) =
    HAdd.hAdd (α := F) (β := F)
      ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (x_1 : Fin 2) ↦ derivWithin f s x : F)
      ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 2 f s x) : F)
⊢ (∑ c : OrderedFinpartition 2,
      (iteratedFDerivWithin 𝕜 c.length g t (f x) : (a : (i : Fin c.length) → E) → F) fun (j : Fin c.length) ↦
        iteratedDerivWithin (c.partSize j) f s x) =
    HAdd.hAdd (α := F) (β := F)
      ((iteratedFDerivWithin 𝕜 2 g t (f x) : (a : (i : Fin 2) → E) → F) fun (x_1 : Fin 2) ↦ derivWithin f s x : F)
      ((fderivWithin 𝕜 g t (f x) : (a : E) → F) (iteratedDerivWithin 2 f s x) : F)

Tactic:
simp only [← (OrderedFinpartition.extendEquiv 1).sum_comp, Fintype.sum_sigma, Fintype.sum_unique,
    OrderedFinpartition.default_eq, OrderedFinpartition.atomic_length, Fintype.sum_option]

Premises used: Fintype.sum_unique, Equiv.sum_comp, Fintype.sum_option, OrderedFinpartition.atomic_length, OrderedFinpartition.extendEquiv, OrderedFinpartition.default_eq, OfNat.ofNat, Fintype.sum_sigma