-- 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 (hn : minSmoothness 𝕜 2 ≤ n)
    {U V W : E → E} {s : Set E} {x : E}
    (hs : UniqueDiffOn 𝕜 s) (h'x : x ∈ closure (interior s)) (hx : x ∈ s)
    (hU : ContDiffWithinAt 𝕜 n U s x) (hV : ContDiffWithinAt 𝕜 n V s x)
    (hW : ContDiffWithinAt 𝕜 n 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:
case h'V
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 V s x

Tactic:
exact hV.isSymmSndFDerivWithinAt hn hs h'x hx

Result:
no goals

Proof state:
case h'W
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 W s x

Tactic:
exact hW.isSymmSndFDerivWithinAt hn hs h'x hx

Result:
no goals

Proof state:
case h'U
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 U s x

Tactic:
exact hU.isSymmSndFDerivWithinAt hn hs h'x hx

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n 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

Tactic:
apply leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt hs hx
  (hU.of_le (le_minSmoothness.trans hn)) (hV.of_le (le_minSmoothness.trans hn))
  (hW.of_le (le_minSmoothness.trans hn))

Result:
case h'U
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 U s x

case h'V
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 V s x

case h'W
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 W s x