Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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
⊢ ((iteratedFDerivWithin 𝕜 3 g t (f x)) fun j ↦
          iteratedDerivWithin ((OrderedFinpartition.atomic 1).extendLeft.extendLeft.partSize j) f s x) +
        (((iteratedFDerivWithin 𝕜 2 g t (f x)) fun j ↦
            iteratedDerivWithin (((OrderedFinpartition.atomic 1).extendLeft.extendMiddle 0).partSize j) f s x) +
          (iteratedFDerivWithin 𝕜 2 g t (f x)) fun j ↦
            iteratedDerivWithin (((OrderedFinpartition.atomic 1).extendLeft.extendMiddle 1).partSize j) f s x) +
      (((iteratedFDerivWithin 𝕜 2 g t (f x)) fun j ↦
          iteratedDerivWithin (((OrderedFinpartition.atomic 1).extendMiddle default).extendLeft.partSize j) f s x) +
        (iteratedFDerivWithin 𝕜 1 g t (f x)) fun j ↦
          iteratedDerivWithin ((((OrderedFinpartition.atomic 1).extendMiddle default).extendMiddle default).partSize j)
            f s x) =
    ((iteratedFDerivWithin 𝕜 3 g t (f x)) fun x_1 ↦ derivWithin f s x) +
          (iteratedFDerivWithin 𝕜 2 g t (f x)) ![iteratedDerivWithin 2 f s x, derivWithin f s x] +
        2 • (iteratedFDerivWithin 𝕜 2 g t (f x)) ![derivWithin f s x, iteratedDerivWithin 2 f s x] +
      (fderivWithin 𝕜 g t (f x)) (iteratedDerivWithin 3 f s x)

Tactic:
simp? [add_assoc, two_smul, iteratedFDerivWithin_one_apply (ht _ <| hst hx)] says
    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]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : 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
⊢ ((iteratedFDerivWithin 𝕜 3 g t (f x)) fun j ↦ iteratedDerivWithin (Fin.cons 1 (Fin.cons 1 fun x ↦ 1) j) f s x) +
      (((iteratedFDerivWithin 𝕜 2 g t (f x)) fun j ↦ iteratedDerivWithin (Fin.cons 2 (fun x ↦ 1) j) f s x) +
        (((iteratedFDerivWithin 𝕜 2 g t (f x)) fun j ↦
            iteratedDerivWithin (update (Fin.cons 1 fun x ↦ 1) 1 2 j) f s x) +
          (((iteratedFDerivWithin 𝕜 2 g t (f x)) fun j ↦
              iteratedDerivWithin (update (Fin.cons 1 fun x ↦ 1) 1 2 j) f s x) +
            (fderivWithin 𝕜 g t (f x)) (iteratedDerivWithin 3 f s x)))) =
    ((iteratedFDerivWithin 𝕜 3 g t (f x)) fun x_1 ↦ derivWithin f s x) +
      ((iteratedFDerivWithin 𝕜 2 g t (f x)) ![iteratedDerivWithin 2 f s x, derivWithin f s x] +
        ((iteratedFDerivWithin 𝕜 2 g t (f x)) ![derivWithin f s x, iteratedDerivWithin 2 f s x] +
          ((iteratedFDerivWithin 𝕜 2 g t (f x)) ![derivWithin f s x, iteratedDerivWithin 2 f s x] +
            (fderivWithin 𝕜 g t (f x)) (iteratedDerivWithin 3 f s x))))