-- Mathlib/Analysis/Calculus/VectorField.lean
/-- The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity
`[U, [V, W]] = [[U, V], W] + [V, [U, W]]`. -/
lemma leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt
    {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) :
    lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W s) s x =
      lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V s) W s x
      + lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W s) s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : 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},
    ContDiffWithinAt 𝕜 2 U s x →
      ContDiffWithinAt 𝕜 2 V s x → DifferentiableWithinAt 𝕜 (fun x => (fderivWithin 𝕜 V s x) (U x)) s x
aux₂ :
  ∀ {U V : E → E},
    ContDiffWithinAt 𝕜 2 U s x →
      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)
⊢ (fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 W s x) (V x)) s x -
          fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 V s x) (W x)) s x)
        (U x) -
      ((fderivWithin 𝕜 U s x) ((fderivWithin 𝕜 W s x) (V x)) - (fderivWithin 𝕜 U s x) ((fderivWithin 𝕜 V s x) (W x))) =
    (fderivWithin 𝕜 W s x) ((fderivWithin 𝕜 V s x) (U x)) - (fderivWithin 𝕜 W s x) ((fderivWithin 𝕜 U s x) (V x)) -
        (fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 V s x) (U x)) s x -
            fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 U s x) (V x)) s x)
          (W x) +
      ((fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 W s x) (U x)) s x -
            fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 U s x) (W x)) s x)
          (V x) -
        ((fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 W s x) (U x)) - (fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 U s x) (W x))))

Tactic:
rw [aux₂ hW hV, aux₂ hV hW, aux₂ hV hU, aux₂ hU hV, aux₂ hW hU, aux₂ hU hW]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : 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},
    ContDiffWithinAt 𝕜 2 U s x →
      ContDiffWithinAt 𝕜 2 V s x → DifferentiableWithinAt 𝕜 (fun x => (fderivWithin 𝕜 V s x) (U x)) s x
aux₂ :
  ∀ {U V : E → E},
    ContDiffWithinAt 𝕜 2 U s x →
      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)
⊢ ((fderivWithin 𝕜 W s x).comp (fderivWithin 𝕜 V s x) + (fderivWithin 𝕜 (fderivWithin 𝕜 W s) s x).flip (V x) -
          ((fderivWithin 𝕜 V s x).comp (fderivWithin 𝕜 W s x) + (fderivWithin 𝕜 (fderivWithin 𝕜 V s) s x).flip (W x)))
        (U x) -
      ((fderivWithin 𝕜 U s x) ((fderivWithin 𝕜 W s x) (V x)) - (fderivWithin 𝕜 U s x) ((fderivWithin 𝕜 V s x) (W x))) =
    (fderivWithin 𝕜 W s x) ((fderivWithin 𝕜 V s x) (U x)) - (fderivWithin 𝕜 W s x) ((fderivWithin 𝕜 U s x) (V x)) -
        ((fderivWithin 𝕜 V s x).comp (fderivWithin 𝕜 U s x) + (fderivWithin 𝕜 (fderivWithin 𝕜 V s) s x).flip (U x) -
            ((fderivWithin 𝕜 U s x).comp (fderivWithin 𝕜 V s x) + (fderivWithin 𝕜 (fderivWithin 𝕜 U s) s x).flip (V x)))
          (W x) +
      (((fderivWithin 𝕜 W s x).comp (fderivWithin 𝕜 U s x) + (fderivWithin 𝕜 (fderivWithin 𝕜 W s) s x).flip (U x) -
            ((fderivWithin 𝕜 U s x).comp (fderivWithin 𝕜 W s x) + (fderivWithin 𝕜 (fderivWithin 𝕜 U s) s x).flip (W x)))
          (V x) -
        ((fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 W s x) (U x)) - (fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 U s x) (W x))))

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
⊢ (fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x)) s x) (U x) -
      ((fderivWithin 𝕜 U s x) ((fderivWithin 𝕜 W s x) (V x)) - (fderivWithin 𝕜 U s x) ((fderivWithin 𝕜 V s x) (W x))) =
    (fderivWithin 𝕜 W s x) ((fderivWithin 𝕜 V s x) (U x)) - (fderivWithin 𝕜 W s x) ((fderivWithin 𝕜 U s x) (V x)) -
        (fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 V s x) (U x) - (fderivWithin 𝕜 U s x) (V x)) s x) (W x) +
      ((fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 W s x) (U x) - (fderivWithin 𝕜 U s x) (W x)) s x) (V x) -
        ((fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 W s x) (U x)) - (fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 U s x) (W x))))

Tactic:
have aux₁ {U V : E → E} (hU : ContDiffWithinAt 𝕜 2 U s x) (hV : ContDiffWithinAt 𝕜 2 V s x) :
    DifferentiableWithinAt 𝕜 (fun x ↦ (fderivWithin 𝕜 V s x) (U x)) s x :=
  have := hV.fderivWithin_right_apply (hU.of_le one_le_two) hs le_rfl hx
  this.differentiableWithinAt le_rfl

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : 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},
    ContDiffWithinAt 𝕜 2 U s x →
      ContDiffWithinAt 𝕜 2 V s x → DifferentiableWithinAt 𝕜 (fun x => (fderivWithin 𝕜 V s x) (U x)) s x
⊢ (fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x)) s x) (U x) -
      ((fderivWithin 𝕜 U s x) ((fderivWithin 𝕜 W s x) (V x)) - (fderivWithin 𝕜 U s x) ((fderivWithin 𝕜 V s x) (W x))) =
    (fderivWithin 𝕜 W s x) ((fderivWithin 𝕜 V s x) (U x)) - (fderivWithin 𝕜 W s x) ((fderivWithin 𝕜 U s x) (V x)) -
        (fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 V s x) (U x) - (fderivWithin 𝕜 U s x) (V x)) s x) (W x) +
      ((fderivWithin 𝕜 (fun x => (fderivWithin 𝕜 W s x) (U x) - (fderivWithin 𝕜 U s x) (W x)) s x) (V x) -
        ((fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 W s x) (U x)) - (fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 U s x) (W x))))