-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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)
⊢ HSub.hSub (α := E)
      ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E) (fderivWithin 𝕜 W s x ∘SL fderivWithin 𝕜 V s x)
                ((ContinuousLinearMap.flip (fderivWithin 𝕜 (fderivWithin 𝕜 W s) s x) : (a : E) → E →L[𝕜] E) (V x) :
                  E →L[𝕜] E) -
              HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E) (fderivWithin 𝕜 V s x ∘SL fderivWithin 𝕜 W s x)
                ((ContinuousLinearMap.flip (fderivWithin 𝕜 (fderivWithin 𝕜 V s) s x) : (a : E) → E →L[𝕜] E) (W x) :
                  E →L[𝕜] E) :
            (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))
        ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E) (fderivWithin 𝕜 V s x ∘SL fderivWithin 𝕜 U s x)
                  ((ContinuousLinearMap.flip (fderivWithin 𝕜 (fderivWithin 𝕜 V s) s x) : (a : E) → E →L[𝕜] E) (U x) :
                    E →L[𝕜] E) -
                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) :
              (a : E) → E)
            (W x) :
          E) +
      HSub.hSub (α := E)
        ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E) (fderivWithin 𝕜 W s x ∘SL fderivWithin 𝕜 U s x)
                  ((ContinuousLinearMap.flip (fderivWithin 𝕜 (fderivWithin 𝕜 W s) s x) : (a : E) → E →L[𝕜] E) (U x) :
                    E →L[𝕜] E) -
                HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E) (fderivWithin 𝕜 U s x ∘SL fderivWithin 𝕜 W s x)
                  ((ContinuousLinearMap.flip (fderivWithin 𝕜 (fderivWithin 𝕜 U s) s x) : (a : E) → E →L[𝕜] E) (W x) :
                    E →L[𝕜] E) :
              (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))
have simp : HAdd.hAdd (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) ((fderivWithin 𝕜 V s x : (a : E) → E) (U x) : E) : E)
        ((((fderivWithin 𝕜 (fderivWithin 𝕜 W s) s x : (a : E) → E →L[𝕜] E) (U x) : E →L[𝕜] E) : (a : E) → E) (V x) :
          E) -
      HAdd.hAdd (α := E) (β := E)
        ((fderivWithin 𝕜 V s x : (a : E) → E) ((fderivWithin 𝕜 W s x : (a : E) → E) (U x) : E) : E)
        ((((fderivWithin 𝕜 (fderivWithin 𝕜 V s) s x : (a : E) → E →L[𝕜] E) (U x) : E →L[𝕜] E) : (a : E) → E) (W 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) (β := 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) -
      (HAdd.hAdd (α := E) (β := E)
          ((fderivWithin 𝕜 V s x : (a : E) → E) ((fderivWithin 𝕜 U s x : (a : E) → E) (W x) : E) : E)
          ((((fderivWithin 𝕜 (fderivWithin 𝕜 V s) s x : (a : E) → E →L[𝕜] E) (U x) : E →L[𝕜] E) : (a : E) → E) (W x) :
            E) -
        HAdd.hAdd (α := E) (β := E)
          ((fderivWithin 𝕜 U s x : (a : E) → E) ((fderivWithin 𝕜 V s x : (a : E) → E) (W x) : E) : E)
          ((((fderivWithin 𝕜 (fderivWithin 𝕜 U s) s x : (a : E) → E →L[𝕜] E) (V x) : E →L[𝕜] E) : (a : E) → E) (W x) :
            E)) +
    (HAdd.hAdd (α := E) (β := E)
          ((fderivWithin 𝕜 W s x : (a : E) → E) ((fderivWithin 𝕜 U s x : (a : E) → E) (V x) : E) : E)
          ((((fderivWithin 𝕜 (fderivWithin 𝕜 W s) s x : (a : E) → E →L[𝕜] E) (U x) : E →L[𝕜] E) : (a : E) → E) (V x) :
            E) -
        HAdd.hAdd (α := E) (β := E)
          ((fderivWithin 𝕜 U s x : (a : E) → E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V x) : E) : E)
          ((((fderivWithin 𝕜 (fderivWithin 𝕜 U s) s x : (a : E) → E →L[𝕜] E) (V x) : E →L[𝕜] E) : (a : E) → E) (W 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: simp only [ContinuousLinearMap.coe_sub', Pi.sub_apply, ContinuousLinearMap.add_apply,
    ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.flip_apply, h'V.eq,
    h'U.eq, h'W.eq]