-- 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
this :
  ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
    Eq (α := ℕ)
      (Fin.cons (α := fun (a : Fin 3) ↦ ℕ) 1 (Fin.cons (α := fun (i : Fin 2) ↦ ℕ) 1 fun (x : Fin 1) ↦ 1) j : ℕ) 1
e_a :
  Eq.{u_2 + 1} (α := (i : Fin 3) → E)
    (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)
    fun (x_1 : Fin 3) ↦ derivWithin f s x
e_a₁ :
  (fun (j : Fin 2) ↦ iteratedDerivWithin (Fin.cons (α := fun (a : Fin 2) ↦ ℕ) 2 (fun (x : Fin 1) ↦ 1) j) f s x) =
    ![iteratedDerivWithin 2 f s x, derivWithin f s x]
e_a₂ :
  (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) =
    ![derivWithin f s x, iteratedDerivWithin 2 f s x]
e_a₃ :
  (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) =
    ![derivWithin f s x, iteratedDerivWithin 2 f s x]
⊢ 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))))

Tactic:
congr