-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 2 U s x
hV : ContDiffWithinAt 𝕜 2 V s x
hW : ContDiffWithinAt 𝕜 2 W s x
h'U : IsSymmSndFDerivWithinAt 𝕜 U s x
h'V : IsSymmSndFDerivWithinAt 𝕜 V s x
h'W : IsSymmSndFDerivWithinAt 𝕜 W s x
aux₁ :
  ∀ {U V : E → E} (hU : ContDiffWithinAt 𝕜 2 U s x) (hV : ContDiffWithinAt 𝕜 2 V s x),
    DifferentiableWithinAt 𝕜 (F := E) (fun (x : E) ↦ (fderivWithin 𝕜 V s x : (a : E) → E) (U x)) s x
aux₂ :
  ∀ {U V : E → E} (hU : ContDiffWithinAt 𝕜 2 U s x) (hV : ContDiffWithinAt 𝕜 2 V s x),
    fderivWithin 𝕜 (fun (y : E) ↦ (fderivWithin 𝕜 U s y : (a : E) → E) (V y)) s x =
      HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E) (fderivWithin 𝕜 U s x ∘SL fderivWithin 𝕜 V s x)
        ((ContinuousLinearMap.flip (fderivWithin 𝕜 (fderivWithin 𝕜 U s) s x) : (a : E) → E →L[𝕜] E) (V x) : E →L[𝕜] E)
rw :
  HSub.hSub (α := E)
      ((HSub.hSub (α := E →L[𝕜] E) (fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 W s x : (a : E) → E) (V x)) s x)
              (fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 V s x : (a : E) → E) (W x)) s x) :
            (a : E) → E)
          (U x) :
        E)
      (HSub.hSub (α := E) (β := E)
        ((fderivWithin 𝕜 U s x : (a : E) → E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V x) : E) : E)
        ((fderivWithin 𝕜 U s x : (a : E) → E) ((fderivWithin 𝕜 V s x : (a : E) → E) (W x) : E) : E)) =
    HSub.hSub (β := E)
        (HSub.hSub (α := E) (β := E)
          ((fderivWithin 𝕜 W s x : (a : E) → E) ((fderivWithin 𝕜 V s x : (a : E) → E) (U x) : E) : E)
          ((fderivWithin 𝕜 W s x : (a : E) → E) ((fderivWithin 𝕜 U s x : (a : E) → E) (V x) : E) : E))
        ((HSub.hSub (α := E →L[𝕜] E) (fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 V s x : (a : E) → E) (U x)) s x)
                (fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 U s x : (a : E) → E) (V x)) s x) :
              (a : E) → E)
            (W x) :
          E) +
      HSub.hSub (α := E)
        ((HSub.hSub (α := E →L[𝕜] E) (fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 W s x : (a : E) → E) (U x)) s x)
                (fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 U s x : (a : E) → E) (W x)) s x) :
              (a : E) → E)
            (V x) :
          E)
        (HSub.hSub (α := E) (β := E)
          ((fderivWithin 𝕜 V s x : (a : E) → E) ((fderivWithin 𝕜 W s x : (a : E) → E) (U x) : E) : E)
          ((fderivWithin 𝕜 V s x : (a : E) → E) ((fderivWithin 𝕜 U s x : (a : E) → E) (W x) : E) : E))
⊢ HSub.hSub (α := E)
      ((HSub.hSub (α := E →L[𝕜] E) (fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 W s x : (a : E) → E) (V x)) s x)
              (fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 V s x : (a : E) → E) (W x)) s x) :
            (a : E) → E)
          (U x) :
        E)
      (HSub.hSub (α := E) (β := E)
        ((fderivWithin 𝕜 U s x : (a : E) → E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V x) : E) : E)
        ((fderivWithin 𝕜 U s x : (a : E) → E) ((fderivWithin 𝕜 V s x : (a : E) → E) (W x) : E) : E)) =
    HSub.hSub (β := E)
        (HSub.hSub (α := E) (β := E)
          ((fderivWithin 𝕜 W s x : (a : E) → E) ((fderivWithin 𝕜 V s x : (a : E) → E) (U x) : E) : E)
          ((fderivWithin 𝕜 W s x : (a : E) → E) ((fderivWithin 𝕜 U s x : (a : E) → E) (V x) : E) : E))
        ((HSub.hSub (α := E →L[𝕜] E) (fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 V s x : (a : E) → E) (U x)) s x)
                (fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 U s x : (a : E) → E) (V x)) s x) :
              (a : E) → E)
            (W x) :
          E) +
      HSub.hSub (α := E)
        ((fderivWithin 𝕜
                (fun (x : E) ↦
                  HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (U x) : E)
                    ((fderivWithin 𝕜 U s x : (a : E) → E) (W x) : E))
                s x :
              (a : E) → E)
            (V x) :
          E)
        (HSub.hSub (α := E) (β := E)
          ((fderivWithin 𝕜 V s x : (a : E) → E) ((fderivWithin 𝕜 W s x : (a : E) → E) (U x) : E) : E)
          ((fderivWithin 𝕜 V s x : (a : E) → E) ((fderivWithin 𝕜 U s x : (a : E) → E) (W x) : E) : E))

Tactic:
rw [fderivWithin_fun_sub (hs x hx) (aux₁ hU hW) (aux₁ hW hU)]

Premises used: fderivWithin_fun_sub