-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (hypothesis)
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
⊢ HSub.hSub (α := E)
      ((fderivWithin 𝕜
              (fun (x : E) ↦
                HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V x) : E)
                  ((fderivWithin 𝕜 V s x : (a : E) → E) (W x) : E))
              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))
        ((fderivWithin 𝕜
                (fun (x : E) ↦
                  HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 V s x : (a : E) → E) (U x) : E)
                    ((fderivWithin 𝕜 U s x : (a : E) → E) (V x) : E))
                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))
have 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)
Tactic: have aux₂ {U V : E → E} (hU : ContDiffWithinAt 𝕜 2 U s x) (hV : ContDiffWithinAt 𝕜 2 V s x) :
      fderivWithin 𝕜 (fun y ↦ (fderivWithin 𝕜 U s y) (V y)) s x =
        (fderivWithin 𝕜 U s x).comp (fderivWithin 𝕜 V s x) +
        (fderivWithin 𝕜 (fderivWithin 𝕜 U s) s x).flip (V x) := by
    refine fderivWithin_clm_apply (hs x hx) ?_ (hV.differentiableWithinAt two_ne_zero)
    exact (hU.fderivWithin_right hs le_rfl hx).differentiableWithinAt one_ne_zero