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
x : E
f : E → 𝕜
hf : DifferentiableAt 𝕜 f x
hV : DifferentiableAt 𝕜 V x
rw :
  -(f x • -lieBracket 𝕜 V W x +
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (((fderiv 𝕜 f x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (W x) : 𝕜) (V x)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-((fderiv 𝕜 f x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (W x) : 𝕜) (V x) +
      f x • lieBracket 𝕜 V W x
⊢ lieBracket 𝕜 (fun (y : E) ↦ f y • V y) W x =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-((fderiv 𝕜 f x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (W x) : 𝕜) (V x) +
      f x • lieBracket 𝕜 V W x

Tactic:
rw [lieBracket_swap, lieBracket_smul_right hf hV, lieBracket_swap, add_comm]

Premises used: VectorField.lieBracket_swap, add_comm, VectorField.lieBracket_smul_right
-- 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
f : E → 𝕜
hf : DifferentiableAt 𝕜 f x
hV : DifferentiableAt 𝕜 V x
⊢ -(f x • -lieBracket 𝕜 V W x +
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (((fderiv 𝕜 f x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (W x) : 𝕜) (V x)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-((fderiv 𝕜 f x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (W x) : 𝕜) (V x) +
      f x • lieBracket 𝕜 V W 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
V W V₁ : E → E
s : Set E
x : E
hV : DifferentiableWithinAt 𝕜 V s x
hV₁ : DifferentiableWithinAt 𝕜 V₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
simp :
  HSub.hSub (β := E)
      (HAdd.hAdd (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V x) : E)
        ((fderivWithin 𝕜 W s x : (a : E) → E) (V₁ x) : E))
      ((fderivWithin 𝕜 (V + V₁) s x : (a : E) → E) (W 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) +
      HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V₁ x) : E)
        ((fderivWithin 𝕜 V₁ s x : (a : E) → E) (W x) : E)
⊢ lieBracketWithin 𝕜 (V + V₁) W s x = lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V₁ W s x

Tactic:
simp only [lieBracketWithin, Pi.add_apply, map_add]

Premises used: map_add, Pi.add_apply, 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₁ : E → E
s : Set E
x : E
hV : DifferentiableWithinAt 𝕜 V s x
hV₁ : DifferentiableWithinAt 𝕜 V₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
rw :
  HAdd.hAdd (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V x) : E)
        ((fderivWithin 𝕜 W s x : (a : E) → E) (V₁ x) : E) -
      HAdd.hAdd (α := E) (β := E) ((fderivWithin 𝕜 V s x : (a : E) → E) (W x) : E)
        ((fderivWithin 𝕜 V₁ s x : (a : E) → E) (W 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) +
      HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V₁ x) : E)
        ((fderivWithin 𝕜 V₁ s x : (a : E) → E) (W x) : E)
⊢ HSub.hSub (β := E)
      (HAdd.hAdd (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V x) : E)
        ((fderivWithin 𝕜 W s x : (a : E) → E) (V₁ x) : E))
      ((fderivWithin 𝕜 (V + V₁) s x : (a : E) → E) (W 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) +
      HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V₁ x) : E)
        ((fderivWithin 𝕜 V₁ s x : (a : E) → E) (W x) : E)

Tactic:
rw [fderivWithin_add hs hV hV₁, ContinuousLinearMap.add_apply]

Premises used: ContinuousLinearMap.add_apply, fderivWithin_add
-- 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₁ : E → E
s : Set E
x : E
hV : DifferentiableWithinAt 𝕜 V s x
hV₁ : DifferentiableWithinAt 𝕜 V₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ HAdd.hAdd (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V x) : E)
        ((fderivWithin 𝕜 W s x : (a : E) → E) (V₁ x) : E) -
      HAdd.hAdd (α := E) (β := E) ((fderivWithin 𝕜 V s x : (a : E) → E) (W x) : E)
        ((fderivWithin 𝕜 V₁ s x : (a : E) → E) (W 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) +
      HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V₁ x) : E)
        ((fderivWithin 𝕜 V₁ s x : (a : E) → E) (W x) : E)

Tactic:
abel
-- 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₁ : E → E
x : E
hV : DifferentiableAt 𝕜 V x
hV₁ : DifferentiableAt 𝕜 V₁ x
simp :
  HSub.hSub (β := E)
      (HAdd.hAdd (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V x) : E) ((fderiv 𝕜 W x : (a : E) → E) (V₁ x) : E))
      ((fderiv 𝕜 (V + V₁) x : (a : E) → E) (W x) : E) =
    HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W x) : E) +
      HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V₁ x) : E) ((fderiv 𝕜 V₁ x : (a : E) → E) (W x) : E)
⊢ lieBracket 𝕜 (V + V₁) W x = lieBracket 𝕜 V W x + lieBracket 𝕜 V₁ W x

Tactic:
simp only [lieBracket, Pi.add_apply, map_add]

Premises used: map_add, Pi.add_apply, 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 V₁ : E → E
x : E
hV : DifferentiableAt 𝕜 V x
hV₁ : DifferentiableAt 𝕜 V₁ x
rw :
  HAdd.hAdd (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V x) : E) ((fderiv 𝕜 W x : (a : E) → E) (V₁ x) : E) -
      HAdd.hAdd (α := E) (β := E) ((fderiv 𝕜 V x : (a : E) → E) (W x) : E) ((fderiv 𝕜 V₁ x : (a : E) → E) (W x) : E) =
    HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W x) : E) +
      HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V₁ x) : E) ((fderiv 𝕜 V₁ x : (a : E) → E) (W x) : E)
⊢ HSub.hSub (β := E)
      (HAdd.hAdd (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V x) : E) ((fderiv 𝕜 W x : (a : E) → E) (V₁ x) : E))
      ((fderiv 𝕜 (V + V₁) x : (a : E) → E) (W x) : E) =
    HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W x) : E) +
      HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V₁ x) : E) ((fderiv 𝕜 V₁ x : (a : E) → E) (W x) : E)

Tactic:
rw [fderiv_add hV hV₁, ContinuousLinearMap.add_apply]

Premises used: ContinuousLinearMap.add_apply, fderiv_add
-- 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₁ : E → E
x : E
hV : DifferentiableAt 𝕜 V x
hV₁ : DifferentiableAt 𝕜 V₁ x
⊢ HAdd.hAdd (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V x) : E) ((fderiv 𝕜 W x : (a : E) → E) (V₁ x) : E) -
      HAdd.hAdd (α := E) (β := E) ((fderiv 𝕜 V x : (a : E) → E) (W x) : E) ((fderiv 𝕜 V₁ x : (a : E) → E) (W x) : E) =
    HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W x) : E) +
      HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V₁ x) : E) ((fderiv 𝕜 V₁ x : (a : E) → E) (W x) : E)

Tactic:
abel
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
W : E → E
s : Set E
h : ∀ (x : E), lieBracketWithin 𝕜 0 W s x = 0 x
⊢ lieBracketWithin 𝕜 0 W s = 0

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
W : E → E
s : Set E
x : E
⊢ lieBracketWithin 𝕜 0 W s x = 0 x

Tactic:
simp [lieBracketWithin]

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
W : E → E
s : Set E
h : ∀ (x : E), lieBracketWithin 𝕜 W 0 s x = 0 x
⊢ lieBracketWithin 𝕜 W 0 s = 0

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
W : E → E
s : Set E
x : E
⊢ lieBracketWithin 𝕜 W 0 s x = 0 x

Tactic:
simp [lieBracketWithin]

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
W : E → E
⊢ lieBracket 𝕜 0 W = 0

Tactic:
simp [← 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
W : E → E
⊢ lieBracket 𝕜 W 0 = 0

Tactic:
simp [← 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 W₁ : E → E
s : Set E
x : E
hW : DifferentiableWithinAt 𝕜 W s x
hW₁ : DifferentiableWithinAt 𝕜 W₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
simp :
  HSub.hSub (α := E) ((fderivWithin 𝕜 (W + W₁) s x : (a : E) → E) (V x) : E)
      (HAdd.hAdd (α := E) (β := E) ((fderivWithin 𝕜 V s x : (a : E) → E) (W x) : E)
        ((fderivWithin 𝕜 V s x : (a : E) → E) (W₁ 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) +
      HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 W₁ s x : (a : E) → E) (V x) : E)
        ((fderivWithin 𝕜 V s x : (a : E) → E) (W₁ x) : E)
⊢ lieBracketWithin 𝕜 V (W + W₁) s x = lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V W₁ s x

Tactic:
simp only [lieBracketWithin, Pi.add_apply, map_add]

Premises used: map_add, Pi.add_apply, 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 W₁ : E → E
s : Set E
x : E
hW : DifferentiableWithinAt 𝕜 W s x
hW₁ : DifferentiableWithinAt 𝕜 W₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
rw :
  HAdd.hAdd (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V x) : E)
        ((fderivWithin 𝕜 W₁ s x : (a : E) → E) (V x) : E) -
      HAdd.hAdd (α := E) (β := E) ((fderivWithin 𝕜 V s x : (a : E) → E) (W x) : E)
        ((fderivWithin 𝕜 V s x : (a : E) → E) (W₁ 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) +
      HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 W₁ s x : (a : E) → E) (V x) : E)
        ((fderivWithin 𝕜 V s x : (a : E) → E) (W₁ x) : E)
⊢ HSub.hSub (α := E) ((fderivWithin 𝕜 (W + W₁) s x : (a : E) → E) (V x) : E)
      (HAdd.hAdd (α := E) (β := E) ((fderivWithin 𝕜 V s x : (a : E) → E) (W x) : E)
        ((fderivWithin 𝕜 V s x : (a : E) → E) (W₁ 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) +
      HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 W₁ s x : (a : E) → E) (V x) : E)
        ((fderivWithin 𝕜 V s x : (a : E) → E) (W₁ x) : E)

Tactic:
rw [fderivWithin_add hs hW hW₁, ContinuousLinearMap.add_apply]

Premises used: ContinuousLinearMap.add_apply, fderivWithin_add
-- 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 W₁ : E → E
s : Set E
x : E
hW : DifferentiableWithinAt 𝕜 W s x
hW₁ : DifferentiableWithinAt 𝕜 W₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ HAdd.hAdd (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V x) : E)
        ((fderivWithin 𝕜 W₁ s x : (a : E) → E) (V x) : E) -
      HAdd.hAdd (α := E) (β := E) ((fderivWithin 𝕜 V s x : (a : E) → E) (W x) : E)
        ((fderivWithin 𝕜 V s x : (a : E) → E) (W₁ 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) +
      HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 W₁ s x : (a : E) → E) (V x) : E)
        ((fderivWithin 𝕜 V s x : (a : E) → E) (W₁ x) : E)

Tactic:
abel
-- 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 W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
simp :
  HSub.hSub (α := E) ((fderiv 𝕜 (W + W₁) x : (a : E) → E) (V x) : E)
      (HAdd.hAdd (α := E) (β := E) ((fderiv 𝕜 V x : (a : E) → E) (W x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W₁ x) : E)) =
    HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W x) : E) +
      HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W₁ x : (a : E) → E) (V x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W₁ x) : E)
⊢ lieBracket 𝕜 V (W + W₁) x = lieBracket 𝕜 V W x + lieBracket 𝕜 V W₁ x

Tactic:
simp only [lieBracket, Pi.add_apply, map_add]

Premises used: map_add, Pi.add_apply, 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 W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
rw :
  HAdd.hAdd (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V x) : E) ((fderiv 𝕜 W₁ x : (a : E) → E) (V x) : E) -
      HAdd.hAdd (α := E) (β := E) ((fderiv 𝕜 V x : (a : E) → E) (W x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W₁ x) : E) =
    HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W x) : E) +
      HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W₁ x : (a : E) → E) (V x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W₁ x) : E)
⊢ HSub.hSub (α := E) ((fderiv 𝕜 (W + W₁) x : (a : E) → E) (V x) : E)
      (HAdd.hAdd (α := E) (β := E) ((fderiv 𝕜 V x : (a : E) → E) (W x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W₁ x) : E)) =
    HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W x) : E) +
      HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W₁ x : (a : E) → E) (V x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W₁ x) : E)

Tactic:
rw [fderiv_add hW hW₁, ContinuousLinearMap.add_apply]

Premises used: ContinuousLinearMap.add_apply, fderiv_add
-- 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 W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
⊢ HAdd.hAdd (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V x) : E) ((fderiv 𝕜 W₁ x : (a : E) → E) (V x) : E) -
      HAdd.hAdd (α := E) (β := E) ((fderiv 𝕜 V x : (a : E) → E) (W x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W₁ x) : E) =
    HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W x : (a : E) → E) (V x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W x) : E) +
      HSub.hSub (α := E) (β := E) ((fderiv 𝕜 W₁ x : (a : E) → E) (V x) : E) ((fderiv 𝕜 V x : (a : E) → E) (W₁ x) : E)

Tactic:
abel
-- 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
⊢ HAdd.hAdd (α := ℕ∞ω) 1 1 ≤ 2

Tactic:
decide
-- 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
⊢ DifferentiableWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) s x

Tactic:
have H₀ : DifferentiableWithinAt 𝕜 (fderivWithin 𝕜 f s) s x :=
    (hf.fderivWithin_right hs (by decide) hxs).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
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
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
have H₁ : UniqueDiffWithinAt 𝕜 s x := hs x hxs
-- 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
rw :
  (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)
hxs₁ : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) s x
hu : DifferentiableWithinAt 𝕜 V s x
hxs₂ : UniqueDiffWithinAt 𝕜 s x
hc₁ : DifferentiableWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) s x
hu₁ : DifferentiableWithinAt 𝕜 W 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:
rw [fderivWithin_clm_apply, fderivWithin_clm_apply]

Premises used: fderivWithin_clm_apply
-- 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
⊢ UniqueDiffWithinAt 𝕜 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
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
⊢ UniqueDiffWithinAt 𝕜 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
⊢ DifferentiableWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) 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
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 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f s) 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
⊢ 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
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 𝕜 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
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:
assumption