-- 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
U V : E → E
hU : ContDiffWithinAt 𝕜 2 U s x
hV : ContDiffWithinAt 𝕜 2 V s x
⊢ DifferentiableWithinAt 𝕜 (fderivWithin 𝕜 U s) s x

Tactic:
exact (hU.fderivWithin_right hs le_rfl hx).differentiableWithinAt le_rfl

Result:
no goals

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 𝕜 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))))

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]

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) ((fderivWithin 𝕜 V s x) (U x)) + ((fderivWithin 𝕜 (fderivWithin 𝕜 W s) s x) (U x)) (V x) -
        ((fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 W s x) (U x)) +
          ((fderivWithin 𝕜 (fderivWithin 𝕜 V s) s x) (U x)) (W 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) ((fderivWithin 𝕜 U s x) (W x)) +
            ((fderivWithin 𝕜 (fderivWithin 𝕜 V s) s x) (U x)) (W x) -
          ((fderivWithin 𝕜 U s x) ((fderivWithin 𝕜 V s x) (W x)) +
            ((fderivWithin 𝕜 (fderivWithin 𝕜 U s) s x) (V x)) (W x))) +
      ((fderivWithin 𝕜 W s x) ((fderivWithin 𝕜 U s x) (V x)) + ((fderivWithin 𝕜 (fderivWithin 𝕜 W s) s x) (U x)) (V x) -
          ((fderivWithin 𝕜 U s x) ((fderivWithin 𝕜 W s x) (V x)) +
            ((fderivWithin 𝕜 (fderivWithin 𝕜 U s) s x) (V x)) (W x)) -
        ((fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 W s x) (U x)) - (fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 U s x) (W x))))