awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W : E → E
m n : ℕ∞ω
hV : ContDiff 𝕜 n V
hW : ContDiff 𝕜 n W
hmn : m + 1 ≤ n
⊢ ContDiff 𝕜 m (lieBracket 𝕜 V W)

Tactic:
contDiff_iff_contDiffAt.2 (fun _ ↦ hV.contDiffAt.lieBracket_vectorField hW.contDiffAt hmn)

Premises used: Iff.mpr, ContDiffAt.lieBracket_vectorField, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W : E → E
s t : Set E
x : E
st : t ∈ 𝓝[s] x
hs : UniqueDiffWithinAt 𝕜 s x
hV : DifferentiableWithinAt 𝕜 V t x
hW : DifferentiableWithinAt 𝕜 W t x
⊢ lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x

Tactic:
simp [lieBracketWithin, fderivWithin_of_mem_nhdsWithin st hs hV,
    fderivWithin_of_mem_nhdsWithin st hs hW]

Premises used: fderivWithin_of_mem_nhdsWithin, VectorField.lieBracketWithin
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W : E → E
s t : Set E
x : E
st : s ⊆ t
ht : UniqueDiffWithinAt 𝕜 s x
hV : DifferentiableWithinAt 𝕜 V t x
hW : DifferentiableWithinAt 𝕜 W t x
⊢ lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x

Tactic:
lieBracketWithin_of_mem_nhdsWithin (nhdsWithin_mono _ st self_mem_nhdsWithin) ht hV hW

Premises used: VectorField.lieBracketWithin_of_mem_nhdsWithin, self_mem_nhdsWithin, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W : E → E
s t : Set E
x : E
ht : t ∈ 𝓝 x
⊢ lieBracketWithin 𝕜 V W (s ∩ t) x = lieBracketWithin 𝕜 V W s x

Tactic:
simp [lieBracketWithin, fderivWithin_inter, ht]

Premises used: fderivWithin_inter, VectorField.lieBracketWithin
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
h : s ∈ 𝓝 x
rw : lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W univ x
rw₁ : lieBracketWithin 𝕜 V W (univ ∩ s) x = lieBracketWithin 𝕜 V W univ x
rw₂ rw₃ : lieBracketWithin 𝕜 V W univ x = lieBracketWithin 𝕜 V W univ x
⊢ lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x

Tactic:
rw [← lieBracketWithin_univ, ← univ_inter s, lieBracketWithin_inter h]

Premises used: VectorField.lieBracketWithin_univ, VectorField.lieBracketWithin_inter, Set.univ_inter
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hx : x ∈ s
⊢ lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x

Tactic:
lieBracketWithin_of_mem_nhds (hs.mem_nhds hx)

Premises used: VectorField.lieBracketWithin_of_mem_nhds, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
hs : UniqueDiffWithinAt 𝕜 s x
hV : DifferentiableAt 𝕜 V x
hW : DifferentiableAt 𝕜 W x
⊢ lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x

Tactic:
simp [lieBracketWithin, lieBracket, fderivWithin_eq_fderiv, hs, hV, hW]

Premises used: fderivWithin_eq_fderiv, VectorField.lieBracketWithin, VectorField.lieBracket
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W : E → E
s t : Set E
x y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x

Tactic:
simp [lieBracketWithin, fderivWithin_congr_set' _ h]

Premises used: fderivWithin_congr_set', VectorField.lieBracketWithin
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W : E → E
s t : Set E
x : E
h : s =ᶠ[𝓝 x] t
⊢ lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x

Tactic:
lieBracketWithin_congr_set' x <| h.filter_mono inf_le_left

Premises used: Filter.EventuallyEq.filter_mono, VectorField.lieBracketWithin_congr_set', inf_le_left
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W : E → E
s t : Set E
x y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ lieBracketWithin 𝕜 V W s =ᶠ[𝓝 x] lieBracketWithin 𝕜 V W t

Tactic:
(eventually_nhds_nhdsWithin.2 h).mono fun _ => lieBracketWithin_congr_set' y

Premises used: Iff.mpr, eventually_nhds_nhdsWithin, Filter.EventuallyEq, VectorField.lieBracketWithin_congr_set', Filter.Eventually.mono
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W : E → E
s t : Set E
x : E
h : s =ᶠ[𝓝 x] t
⊢ lieBracketWithin 𝕜 V W s =ᶠ[𝓝 x] lieBracketWithin 𝕜 V W t

Tactic:
lieBracketWithin_eventually_congr_set' x <| h.filter_mono inf_le_left

Premises used: Filter.EventuallyEq.filter_mono, VectorField.lieBracketWithin_eventually_congr_set', inf_le_left
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s t : Set E
x : E
hV : DifferentiableWithinAt 𝕜 V s x
hVs : EqOn V₁ V t
hVx : V₁ x = V x
hW : DifferentiableWithinAt 𝕜 W s x
hWs : EqOn W₁ W t
hWx : W₁ x = W x
hxt : UniqueDiffWithinAt 𝕜 t x
h₁ : t ⊆ s
⊢ lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W s x

Tactic:
simp [lieBracketWithin, hV.fderivWithin_congr_mono, hW.fderivWithin_congr_mono, hVs, hVx,
    hWs, hWx, hxt, h₁]

Premises used: DifferentiableWithinAt.fderivWithin_congr_mono, VectorField.lieBracketWithin
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s : Set E
x : E
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
⊢ lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x

Tactic:
simp only [lieBracketWithin, hV.fderivWithin_eq hxV, hW.fderivWithin_eq hxW, hxV, hxW]

Premises used: Filter.EventuallyEq.fderivWithin_eq, VectorField.lieBracketWithin
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s : Set E
x : E
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
hx : x ∈ s
⊢ lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x

Tactic:
hV.lieBracketWithin_vectorField_eq (mem_of_mem_nhdsWithin hx hV :)
    hW (mem_of_mem_nhdsWithin hx hW :)

Premises used: mem_of_mem_nhdsWithin, Filter.EventuallyEq.lieBracketWithin_vectorField_eq
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s t : Set E
x : E
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
h :
  ∀ (x : E) (hV' : Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 V₁ t x) (fderivWithin 𝕜 V t x))
    (hW' : Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 W₁ t x) (fderivWithin 𝕜 W t x)) (hV : V₁ x = V x) (hW : W₁ x = W x),
    lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W t x
⊢ lieBracketWithin 𝕜 V₁ W₁ t =ᶠ[𝓝[s] x] lieBracketWithin 𝕜 V W t

Tactic:
filter_upwards [hV.fderivWithin' ht (𝕜 := 𝕜), hW.fderivWithin' ht (𝕜 := 𝕜), hV, hW]
    with x hV' hW' hV hW

Premises used: Filter.EventuallyEq.fderivWithin'
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s t : Set E
x_1 : E
hV_1 : V₁ =ᶠ[𝓝[s] x_1] V
hW_1 : W₁ =ᶠ[𝓝[s] x_1] W
ht : t ⊆ s
x : E
hV' : Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 V₁ t x) (fderivWithin 𝕜 V t x)
hW' : Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 W₁ t x) (fderivWithin 𝕜 W t x)
hV : V₁ x = V x
hW : W₁ x = W x
⊢ lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W t x

Tactic:
simp [lieBracketWithin, hV', hW', hV, hW]

Premises used: VectorField.lieBracketWithin
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s : Set E
x : E
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
⊢ lieBracketWithin 𝕜 V₁ W₁ s =ᶠ[𝓝[s] x] lieBracketWithin 𝕜 V W s

Tactic:
hV.lieBracketWithin_vectorField' hW Subset.rfl

Premises used: Set.Subset.rfl, Filter.EventuallyEq.lieBracketWithin_vectorField'
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s : Set E
x : E
hV : V₁ =ᶠ[𝓝[insert x s] x] V
hW : W₁ =ᶠ[𝓝[insert x s] x] W
⊢ lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x

Tactic:
apply mem_of_mem_nhdsWithin (mem_insert x s) (hV.lieBracketWithin_vectorField' hW
    (subset_insert x s))

Premises used: mem_of_mem_nhdsWithin, Set.mem_insert, Set.subset_insert, Filter.EventuallyEq.lieBracketWithin_vectorField'
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s : Set E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
⊢ lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x

Tactic:
(hV.filter_mono nhdsWithin_le_nhds).lieBracketWithin_vectorField_eq hV.self_of_nhds
    (hW.filter_mono nhdsWithin_le_nhds) hW.self_of_nhds

Premises used: Filter.EventuallyEq.filter_mono, Filter.Eventually.self_of_nhds, nhdsWithin_le_nhds, Filter.EventuallyEq.lieBracketWithin_vectorField_eq
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s : Set E
x : E
hV : EqOn V₁ V s
hVx : V₁ x = V x
hW : EqOn W₁ W s
hWx : W₁ x = W x
⊢ lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x

Tactic:
(hV.eventuallyEq.filter_mono inf_le_right).lieBracketWithin_vectorField_eq hVx
    (hW.eventuallyEq.filter_mono inf_le_right) hWx

Premises used: Filter.EventuallyEq.filter_mono, Set.EqOn.eventuallyEq, inf_le_right, Filter.EventuallyEq.lieBracketWithin_vectorField_eq
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s : Set E
x : E
hV : EqOn V₁ V s
hW : EqOn W₁ W s
hx : x ∈ s
⊢ lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x

Tactic:
lieBracketWithin_congr hV (hV hx) hW (hW hx)

Premises used: VectorField.lieBracketWithin_congr
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
rw : lieBracketWithin 𝕜 V₁ W₁ univ x = lieBracket 𝕜 V W x
rw₁ : lieBracketWithin 𝕜 V₁ W₁ univ x = lieBracketWithin 𝕜 V W univ x
rw₂ rw₃ : lieBracketWithin 𝕜 V W univ x = lieBracketWithin 𝕜 V W univ x
⊢ lieBracket 𝕜 V₁ W₁ x = lieBracket 𝕜 V W x

Tactic:
rw [← lieBracketWithin_univ, ← lieBracketWithin_univ, hV.lieBracketWithin_vectorField_eq_nhds hW]

Premises used: VectorField.lieBracketWithin_univ, Filter.EventuallyEq.lieBracketWithin_vectorField_eq_nhds
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
h : ∀ (y : E) (hVy : V₁ =ᶠ[𝓝 y] V) (hWy : W₁ =ᶠ[𝓝 y] W), lieBracket 𝕜 V₁ W₁ y = lieBracket 𝕜 V W y
⊢ lieBracket 𝕜 V₁ W₁ =ᶠ[𝓝 x] lieBracket 𝕜 V W

Tactic:
filter_upwards [hV.eventuallyEq_nhds, hW.eventuallyEq_nhds] with y hVy hWy

Premises used: Filter.EventuallyEq.eventuallyEq_nhds
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
y : E
hVy : V₁ =ᶠ[𝓝 y] V
hWy : W₁ =ᶠ[𝓝 y] W
⊢ lieBracket 𝕜 V₁ W₁ y = lieBracket 𝕜 V W y

Tactic:
hVy.lieBracket_vectorField_eq hWy

Premises used: Filter.EventuallyEq.lieBracket_vectorField_eq
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
y : E
hVy : V₁ =ᶠ[𝓝 y] V
hWy : W₁ =ᶠ[𝓝 y] W
⊢ lieBracket 𝕜 V₁ W₁ y = lieBracket 𝕜 V W y

Tactic:
exact hVy.lieBracket_vectorField_eq hWy

Premises used: Filter.EventuallyEq.lieBracket_vectorField_eq
-- Module: Mathlib.Analysis.Calculus.VectorField
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
simp :
  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))
⊢ 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:
simp only [lieBracketWithin_eq, map_sub]

Premises used: map_sub, VectorField.lieBracketWithin_eq
-- Module: Mathlib.Analysis.Calculus.VectorField
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
⊢ ∀ {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

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 one_ne_zero
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U_1 V_1 W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hU_1 : ContDiffWithinAt 𝕜 2 U_1 s x
hV_1 : ContDiffWithinAt 𝕜 2 V_1 s x
hW : ContDiffWithinAt 𝕜 2 W s x
h'U : IsSymmSndFDerivWithinAt 𝕜 U_1 s x
h'V : IsSymmSndFDerivWithinAt 𝕜 V_1 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
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:
fderivWithin_clm_apply (hs x hx) ?_ (hV.differentiableWithinAt two_ne_zero)

Premises used: two_ne_zero, fderivWithin_clm_apply, ContDiffWithinAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U_1 V_1 W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hU_1 : ContDiffWithinAt 𝕜 2 U_1 s x
hV_1 : ContDiffWithinAt 𝕜 2 V_1 s x
hW : ContDiffWithinAt 𝕜 2 W s x
h'U : IsSymmSndFDerivWithinAt 𝕜 U_1 s x
h'V : IsSymmSndFDerivWithinAt 𝕜 V_1 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
U V : E → E
hU : ContDiffWithinAt 𝕜 2 U s x
hV : ContDiffWithinAt 𝕜 2 V s x
refine : DifferentiableWithinAt 𝕜 (F := E →L[𝕜] E) (fderivWithin 𝕜 U s) 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:
refine fderivWithin_clm_apply (hs x hx) ?_ (hV.differentiableWithinAt two_ne_zero)

Premises used: two_ne_zero, fderivWithin_clm_apply, ContDiffWithinAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U_1 V_1 W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hU_1 : ContDiffWithinAt 𝕜 2 U_1 s x
hV_1 : ContDiffWithinAt 𝕜 2 V_1 s x
hW : ContDiffWithinAt 𝕜 2 W s x
h'U : IsSymmSndFDerivWithinAt 𝕜 U_1 s x
h'V : IsSymmSndFDerivWithinAt 𝕜 V_1 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
U V : E → E
hU : ContDiffWithinAt 𝕜 2 U s x
hV : ContDiffWithinAt 𝕜 2 V s x
⊢ DifferentiableWithinAt 𝕜 (F := E →L[𝕜] E) (fderivWithin 𝕜 U s) s x

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

Premises used: one_ne_zero, ContDiffWithinAt.differentiableWithinAt, ContDiffWithinAt.fderivWithin_right
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
U_1 V_1 W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hU_1 : ContDiffWithinAt 𝕜 2 U_1 s x
hV_1 : ContDiffWithinAt 𝕜 2 V_1 s x
hW : ContDiffWithinAt 𝕜 2 W s x
h'U : IsSymmSndFDerivWithinAt 𝕜 U_1 s x
h'V : IsSymmSndFDerivWithinAt 𝕜 V_1 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
U V : E → E
hU : ContDiffWithinAt 𝕜 2 U s x
hV : ContDiffWithinAt 𝕜 2 V s x
⊢ DifferentiableWithinAt 𝕜 (F := E →L[𝕜] E) (fderivWithin 𝕜 U s) s x

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

Premises used: one_ne_zero, ContDiffWithinAt.differentiableWithinAt, ContDiffWithinAt.fderivWithin_right
-- Module: Mathlib.Analysis.Calculus.VectorField
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
⊢ ∀ {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
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n 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

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

Premises used: ContDiffWithinAt.of_le, le_minSmoothness, VectorField.leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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:
hU.isSymmSndFDerivWithinAt hn hs h'x hx

Premises used: ContDiffWithinAt.isSymmSndFDerivWithinAt