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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
s : Set E
x : E
f : E → F
hf : ContDiffWithinAt 𝕜 2 f s x
hsymm : IsSymmSndFDerivWithinAt 𝕜 f s x
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
H₀ : DifferentiableWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) s x
H₁ : UniqueDiffWithinAt 𝕜 s x
⊢ DifferentiableWithinAt 𝕜 W s x

Tactic:
try assumption
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
s : Set E
x : E
f : E → F
hf : ContDiffWithinAt 𝕜 2 f s x
hsymm : IsSymmSndFDerivWithinAt 𝕜 f s x
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
H₀ : DifferentiableWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) s x
H₁ : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 f s x : (a : E) → F) (lieBracketWithin 𝕜 V W s x) =
    HSub.hSub (α := F) (β := F)
      ((HAdd.hAdd (α := E →L[𝕜] F) (β := E →L[𝕜] F) (fderivWithin 𝕜 f s x ∘SL fderivWithin 𝕜 W s x)
              ((ContinuousLinearMap.flip (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) : (a : E) → E →L[𝕜] F) (W x) :
                E →L[𝕜] F) :
            (a : E) → F)
          (V x) :
        F)
      ((HAdd.hAdd (α := E →L[𝕜] F) (β := E →L[𝕜] F) (fderivWithin 𝕜 f s x ∘SL fderivWithin 𝕜 V s x)
              ((ContinuousLinearMap.flip (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) : (a : E) → E →L[𝕜] F) (V x) :
                E →L[𝕜] F) :
            (a : E) → F)
          (W x) :
        F)

Tactic:
simp [lieBracketWithin, hsymm (V _) (W _)]

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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
hf : ContDiffAt 𝕜 2 f x
hsymm : IsSymmSndFDerivAt 𝕜 f x
hW : DifferentiableAt 𝕜 W x
hV : DifferentiableAt 𝕜 V x
simp :
  ∀ (hf : ContDiffWithinAt 𝕜 2 f univ x) (hsymm : IsSymmSndFDerivWithinAt 𝕜 f univ x)
    (hW : DifferentiableWithinAt 𝕜 W univ x) (hV : DifferentiableWithinAt 𝕜 V univ x),
    (fderivWithin 𝕜 f univ x : (a : E) → F) (lieBracketWithin 𝕜 V W univ x) =
      HSub.hSub (α := F) (β := F)
        ((fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 f univ x : (a : E) → F) (W x)) univ x : (a : E) → F) (V x) : F)
        ((fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 f univ x : (a : E) → F) (V x)) univ x : (a : E) → F) (W x) : F)
⊢ (fderiv 𝕜 f x : (a : E) → F) (lieBracket 𝕜 V W x) =
    HSub.hSub (α := F) (β := F)
      ((fderiv 𝕜 (fun (x : E) ↦ (fderiv 𝕜 f x : (a : E) → F) (W x)) x : (a : E) → F) (V x) : F)
      ((fderiv 𝕜 (fun (x : E) ↦ (fderiv 𝕜 f x : (a : E) → F) (V x)) x : (a : E) → F) (W x) : F)

Tactic:
simp only [← fderivWithin_univ, ← lieBracketWithin_univ, ← contDiffWithinAt_univ,
    ← isSymmSndFDerivWithinAt_univ, ← differentiableWithinAt_univ] at *

Premises used: isSymmSndFDerivWithinAt_univ, contDiffWithinAt_univ, VectorField.lieBracketWithin_univ, fderivWithin_univ, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
hf : ContDiffWithinAt 𝕜 2 f univ x
hsymm : IsSymmSndFDerivWithinAt 𝕜 f univ x
hW : DifferentiableWithinAt 𝕜 W univ x
hV : DifferentiableWithinAt 𝕜 V univ x
⊢ UniqueDiffOn.{u_1, u_2} 𝕜 (E := E) univ

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
hf : ContDiffWithinAt 𝕜 2 f univ x
hsymm : IsSymmSndFDerivWithinAt 𝕜 f univ x
hW : DifferentiableWithinAt 𝕜 W univ x
hV : DifferentiableWithinAt 𝕜 V univ x
⊢ Membership.mem (γ := Set E) univ x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
hf : ContDiffWithinAt 𝕜 2 f univ x
hsymm : IsSymmSndFDerivWithinAt 𝕜 f univ x
hW : DifferentiableWithinAt 𝕜 W univ x
hV : DifferentiableWithinAt 𝕜 V univ x
⊢ (fderivWithin 𝕜 f univ x : (a : E) → F) (lieBracketWithin 𝕜 V W univ x) =
    HSub.hSub (α := F) (β := F)
      ((fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 f univ x : (a : E) → F) (W x)) univ x : (a : E) → F) (V x) : F)
      ((fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 f univ x : (a : E) → F) (V x)) univ x : (a : E) → F) (W x) : F)

Tactic:
exact fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt hf hsymm (by simp) (by simp)
    hW hV

Premises used: VectorField.fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
s : Set E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hxs' : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
hf₁ : ContDiffWithinAt 𝕜 2 f s x
hsymm : IsSymmSndFDerivWithinAt 𝕜 f s x
hs₁ : UniqueDiffOn 𝕜 s
hxs₁ : x ∈ s
hW₁ : DifferentiableWithinAt 𝕜 W s x
hV₁ : DifferentiableWithinAt 𝕜 V s x
⊢ (fderivWithin 𝕜 f s x : (a : E) → F) (lieBracketWithin 𝕜 V W s x) =
    HSub.hSub (α := F) (β := F)
      ((fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 f s x : (a : E) → F) (W x)) s x : (a : E) → F) (V x) : F)
      ((fderivWithin 𝕜 (fun (x : E) ↦ (fderivWithin 𝕜 f s x : (a : E) → F) (V x)) s x : (a : E) → F) (W x) : F)

Tactic:
apply fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt

Premises used: VectorField.fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
s : Set E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hxs' : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
⊢ UniqueDiffOn 𝕜 s

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
s : Set E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hxs' : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
⊢ UniqueDiffOn 𝕜 s

Tactic:
try assumption
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
s : Set E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hxs' : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
⊢ x ∈ s

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
s : Set E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hxs' : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
⊢ x ∈ s

Tactic:
try assumption
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
s : Set E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hxs' : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
⊢ DifferentiableWithinAt 𝕜 W s x

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
s : Set E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hxs' : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
⊢ DifferentiableWithinAt 𝕜 W s x

Tactic:
try assumption
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
s : Set E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hxs' : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
⊢ DifferentiableWithinAt 𝕜 V s x

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
s : Set E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hxs' : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
⊢ DifferentiableWithinAt 𝕜 V s x

Tactic:
try assumption
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
s : Set E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hxs' : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
⊢ ContDiffWithinAt 𝕜 2 f s x

Tactic:
hf.of_le <| le_minSmoothness.trans hn

Premises used: ContDiffWithinAt.of_le, le_minSmoothness, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
s : Set E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hxs' : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x

Tactic:
hf.isSymmSndFDerivWithinAt hn hs hxs' hxs

Premises used: ContDiffWithinAt.isSymmSndFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
s : Set E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hxs' : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
⊢ ContDiffWithinAt 𝕜 2 f s x

Tactic:
exacts [hf.of_le <| le_minSmoothness.trans hn, hf.isSymmSndFDerivWithinAt hn hs hxs' hxs]

Premises used: ContDiffWithinAt.of_le, le_minSmoothness, ContDiffWithinAt.isSymmSndFDerivWithinAt, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
hW : DifferentiableAt 𝕜 W x
hV : DifferentiableAt 𝕜 V x
hf₁ : ContDiffAt 𝕜 2 f x
hsymm : IsSymmSndFDerivAt 𝕜 f x
hW₁ : DifferentiableAt 𝕜 W x
hV₁ : DifferentiableAt 𝕜 V x
⊢ (fderiv 𝕜 f x : (a : E) → F) (lieBracket 𝕜 V W x) =
    HSub.hSub (α := F) (β := F)
      ((fderiv 𝕜 (fun (x : E) ↦ (fderiv 𝕜 f x : (a : E) → F) (W x)) x : (a : E) → F) (V x) : F)
      ((fderiv 𝕜 (fun (x : E) ↦ (fderiv 𝕜 f x : (a : E) → F) (V x)) x : (a : E) → F) (W x) : F)

Tactic:
apply fderiv_apply_lieBracket_of_isSymmSndFDerivAt

Premises used: VectorField.fderiv_apply_lieBracket_of_isSymmSndFDerivAt
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
hW : DifferentiableAt 𝕜 W x
hV : DifferentiableAt 𝕜 V x
⊢ DifferentiableAt 𝕜 W x

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
hW : DifferentiableAt 𝕜 W x
hV : DifferentiableAt 𝕜 V x
⊢ DifferentiableAt 𝕜 W x

Tactic:
try assumption
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
hW : DifferentiableAt 𝕜 W x
hV : DifferentiableAt 𝕜 V x
⊢ DifferentiableAt 𝕜 V x

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
hW : DifferentiableAt 𝕜 W x
hV : DifferentiableAt 𝕜 V x
⊢ DifferentiableAt 𝕜 V x

Tactic:
try assumption
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
hW : DifferentiableAt 𝕜 W x
hV : DifferentiableAt 𝕜 V x
⊢ ContDiffAt 𝕜 2 f x

Tactic:
hf.of_le <| le_minSmoothness.trans hn

Premises used: le_minSmoothness, ContDiffAt.of_le, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
hW : DifferentiableAt 𝕜 W x
hV : DifferentiableAt 𝕜 V x
⊢ IsSymmSndFDerivAt 𝕜 f x

Tactic:
hf.isSymmSndFDerivAt hn

Premises used: ContDiffAt.isSymmSndFDerivAt
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
hW : DifferentiableAt 𝕜 W x
hV : DifferentiableAt 𝕜 V x
⊢ ContDiffAt 𝕜 2 f x

Tactic:
exacts [hf.of_le <| le_minSmoothness.trans hn, hf.isSymmSndFDerivAt hn]

Premises used: ContDiffAt.isSymmSndFDerivAt, le_minSmoothness, ContDiffAt.of_le, LE.le.trans
-- 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
m n : ℕ∞ω
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx : x ∈ s
hf : ContDiffWithinAt 𝕜 (F := E) m (fun (x : E) ↦ (fderivWithin 𝕜 W s x : (a : E) → E) (V x)) s x
hg : ContDiffWithinAt 𝕜 (F := E) m (fun (x : E) ↦ (fderivWithin 𝕜 V s x : (a : E) → E) (W x)) s x
⊢ ContDiffWithinAt 𝕜 m (lieBracketWithin 𝕜 V W s) s x

Tactic:
apply ContDiffWithinAt.sub

Premises used: ContDiffWithinAt.sub
-- 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
m n : ℕ∞ω
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (F := E) m (fun (x : E) ↦ (fderivWithin 𝕜 W s x : (a : E) → E) (V x)) s x

Tactic:
ContDiffWithinAt.clm_apply (hW.fderivWithin_right hs hmn hx)
      (hV.of_le (le_trans le_self_add hmn))

Premises used: ContDiffWithinAt.clm_apply, ContDiffWithinAt.of_le, le_self_add, ContDiffWithinAt.fderivWithin_right, le_trans
-- 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
m n : ℕ∞ω
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (F := E) m (fun (x : E) ↦ (fderivWithin 𝕜 W s x : (a : E) → E) (V x)) s x

Tactic:
exact ContDiffWithinAt.clm_apply (hW.fderivWithin_right hs hmn hx)
      (hV.of_le (le_trans le_self_add hmn))

Premises used: ContDiffWithinAt.clm_apply, ContDiffWithinAt.of_le, le_self_add, ContDiffWithinAt.fderivWithin_right, le_trans
-- 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
m n : ℕ∞ω
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (F := E) m (fun (x : E) ↦ (fderivWithin 𝕜 V s x : (a : E) → E) (W x)) s x

Tactic:
ContDiffWithinAt.clm_apply (hV.fderivWithin_right hs hmn hx)
      (hW.of_le (le_trans le_self_add hmn))

Premises used: ContDiffWithinAt.clm_apply, ContDiffWithinAt.of_le, le_self_add, ContDiffWithinAt.fderivWithin_right, le_trans
-- 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
m n : ℕ∞ω
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (F := E) m (fun (x : E) ↦ (fderivWithin 𝕜 V s x : (a : E) → E) (W x)) s x

Tactic:
exact ContDiffWithinAt.clm_apply (hV.fderivWithin_right hs hmn hx)
      (hW.of_le (le_trans le_self_add hmn))

Premises used: ContDiffWithinAt.clm_apply, ContDiffWithinAt.of_le, le_self_add, ContDiffWithinAt.fderivWithin_right, le_trans
-- 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
x : E
m n : ℕ∞ω
hV : ContDiffAt 𝕜 n V x
hW : ContDiffAt 𝕜 n W x
hmn : m + 1 ≤ n
⊢ ContDiffWithinAt 𝕜 n V univ x

Tactic:
rw [← contDiffWithinAt_univ] at hV hW ⊢

Premises used: contDiffWithinAt_univ
-- 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
x : E
m n : ℕ∞ω
hV : ContDiffAt 𝕜 n V x
hW : ContDiffAt 𝕜 n W x
hmn : m + 1 ≤ n
hV₁ : ContDiffWithinAt 𝕜 n V univ x
⊢ ContDiffWithinAt 𝕜 n W univ x

Tactic:
rw [← contDiffWithinAt_univ] at hV hW ⊢

Premises used: contDiffWithinAt_univ
-- 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
x : E
m n : ℕ∞ω
hV : ContDiffAt 𝕜 n V x
hW : ContDiffAt 𝕜 n W x
hmn : m + 1 ≤ n
hV₁ : ContDiffWithinAt 𝕜 n V univ x
hW₁ : ContDiffWithinAt 𝕜 n W univ x
⊢ m + 1 ≤ n

Tactic:
rw [← contDiffWithinAt_univ] at hV hW ⊢

Premises used: contDiffWithinAt_univ
-- 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
x : E
m n : ℕ∞ω
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
hmn : m + 1 ≤ n
simp_rw : ContDiffWithinAt 𝕜 m (lieBracketWithin 𝕜 V W univ) univ x
⊢ ContDiffWithinAt 𝕜 m (lieBracket 𝕜 V W) univ x

Tactic:
simp_rw [← lieBracketWithin_univ]

Premises used: VectorField.lieBracketWithin_univ
-- 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
x : E
m n : ℕ∞ω
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
hmn : m + 1 ≤ n
⊢ ContDiffWithinAt 𝕜 m (lieBracketWithin 𝕜 V W univ) univ x

Tactic:
hV.lieBracketWithin_vectorField hW uniqueDiffOn_univ hmn (mem_univ _)

Premises used: ContDiffWithinAt.lieBracketWithin_vectorField, uniqueDiffOn_univ, Set.mem_univ
-- 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
x : E
m n : ℕ∞ω
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
hmn : m + 1 ≤ n
⊢ ContDiffWithinAt 𝕜 m (lieBracketWithin 𝕜 V W univ) univ x

Tactic:
exact hV.lieBracketWithin_vectorField hW uniqueDiffOn_univ hmn (mem_univ _)

Premises used: ContDiffWithinAt.lieBracketWithin_vectorField, uniqueDiffOn_univ, Set.mem_univ
-- 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
m n : ℕ∞ω
hV : ContDiffOn 𝕜 n V s
hW : ContDiffOn 𝕜 n W s
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
⊢ ContDiffOn 𝕜 m (lieBracketWithin 𝕜 V W s) s

Tactic:
fun x hx ↦ (hV x hx).lieBracketWithin_vectorField (hW x hx) hs hmn hx

Premises used: ContDiffOn, ContDiffWithinAt.lieBracketWithin_vectorField