awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
f' : F
h : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) 0
c : 𝕜
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ c • t
s' : Set 𝕜 := (fun (t : 𝕜) ↦ x + t • v) ⁻¹' s
A : HasDerivAt g c 0
B : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' s' (g 0)
Z :
  HasDerivWithinAt (fun (x_1 : 𝕜) ↦ f (x + x_1 • c • v)) (c • f')
    (preimage (β := 𝕜) (fun (t : 𝕜) ↦ t * c) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s)) 0
h₁ :
  ∀ (t : 𝕜),
    Membership.mem (γ := Set 𝕜) ((fun (t : 𝕜) ↦ x + t • c • v) ⁻¹' s) t ↔
      Membership.mem (γ := Set 𝕜) (preimage (β := 𝕜) (fun (t : 𝕜) ↦ t * c) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s)) t
⊢ Eq.{u_1 + 1} (α := Set 𝕜) ((fun (t : 𝕜) ↦ x + t • c • v) ⁻¹' s)
    (preimage (β := 𝕜) (fun (t : 𝕜) ↦ t * c) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s))

Tactic:
ext t
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
f' : F
h : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) 0
c : 𝕜
g : (t : 𝕜) → 𝕜 := fun (t : 𝕜) ↦ c • t
s' : Set 𝕜 := (fun (t : 𝕜) ↦ x + t • v) ⁻¹' s
A : HasDerivAt g c 0
B : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' s' (g 0)
Z :
  HasDerivWithinAt (fun (x_1 : 𝕜) ↦ f (x + x_1 • c • v)) (c • f')
    (preimage (β := 𝕜) (fun (t : 𝕜) ↦ t * c) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s)) 0
t : 𝕜
⊢ Membership.mem (γ := Set 𝕜) ((fun (t : 𝕜) ↦ x + t • c • v) ⁻¹' s) t ↔
    Membership.mem (γ := Set 𝕜) (preimage (β := 𝕜) (fun (t : 𝕜) ↦ t * c) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s)) t

Tactic:
simp [← smul_smul]

Premises used: smul_smul
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
f' : F
c : 𝕜
hc : c ≠ 0
h : HasLineDerivWithinAt 𝕜 f (c • f') s x (c • v)
⊢ HasLineDerivWithinAt 𝕜 f f' s x v

Tactic:
simpa [smul_smul, inv_mul_cancel₀ hc] using h.smul (c ⁻¹)

Premises used: smul_smul, HasLineDerivWithinAt.smul, Inv.inv, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
f' : F
h : HasLineDerivAt 𝕜 f f' x v
c : 𝕜
simp : ∀ (h : HasLineDerivWithinAt 𝕜 f f' univ x v), HasLineDerivWithinAt 𝕜 f (c • f') univ x (c • v)
⊢ HasLineDerivAt 𝕜 f (c • f') x (c • v)

Tactic:
simp only [← hasLineDerivWithinAt_univ] at h ⊢

Premises used: hasLineDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
f' : F
c : 𝕜
h : HasLineDerivWithinAt 𝕜 f f' univ x v
⊢ HasLineDerivWithinAt 𝕜 f (c • f') univ x (c • v)

Tactic:
HasLineDerivWithinAt.smul h c

Premises used: HasLineDerivWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
f' : F
c : 𝕜
h : HasLineDerivWithinAt 𝕜 f f' univ x v
⊢ HasLineDerivWithinAt 𝕜 f (c • f') univ x (c • v)

Tactic:
exact HasLineDerivWithinAt.smul h c

Premises used: HasLineDerivWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
f' : F
c : 𝕜
hc : c ≠ 0
h : HasLineDerivAt 𝕜 f (c • f') x (c • v)
⊢ HasLineDerivAt 𝕜 f f' x v

Tactic:
simpa [smul_smul, inv_mul_cancel₀ hc] using h.smul (c ⁻¹)

Premises used: smul_smul, Inv.inv, HasLineDerivAt.smul, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
h : LineDifferentiableWithinAt 𝕜 f s x v
c : 𝕜
⊢ LineDifferentiableWithinAt 𝕜 f s x (c • v)

Tactic:
(h.hasLineDerivWithinAt.smul c).lineDifferentiableWithinAt

Premises used: LineDifferentiableWithinAt.hasLineDerivWithinAt, HasLineDerivWithinAt.lineDifferentiableWithinAt, HasLineDerivWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
s : Set E
x v : E
c : 𝕜
hc : c ≠ 0
h : LineDifferentiableWithinAt 𝕜 f s x (c • v)
⊢ LineDifferentiableWithinAt 𝕜 f s x v

Tactic:
simpa [smul_smul, inv_mul_cancel₀ hc] using h.smul (c ⁻¹)

Premises used: LineDifferentiableWithinAt.smul, smul_smul, Inv.inv, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
h : LineDifferentiableAt 𝕜 f x v
c : 𝕜
⊢ LineDifferentiableAt 𝕜 f x (c • v)

Tactic:
(h.hasLineDerivAt.smul c).lineDifferentiableAt

Premises used: HasLineDerivAt.lineDifferentiableAt, LineDifferentiableAt.hasLineDerivAt, HasLineDerivAt.smul
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
h : LineDifferentiableAt 𝕜 f x (c • v)
⊢ LineDifferentiableAt 𝕜 f x v

Tactic:
simpa [smul_smul, inv_mul_cancel₀ hc] using h.smul (c ⁻¹)

Premises used: smul_smul, Inv.inv, inv_mul_cancel₀, LineDifferentiableAt.smul
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
inl :
  lineDeriv 𝕜 f x (HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (lineDeriv 𝕜 f x v)
inr : ∀ (hc : c ≠ 0), lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v

Tactic:
rcases eq_or_ne c 0 with rfl | hc

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
⊢ lineDeriv 𝕜 f x (HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (lineDeriv 𝕜 f x v)

Tactic:
simp [lineDeriv_zero]

Premises used: lineDeriv_zero
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
pos : ∀ (H : LineDifferentiableAt 𝕜 f x v), lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
neg : ∀ (H : ¬LineDifferentiableAt 𝕜 f x v), lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v

Tactic:
by_cases H : LineDifferentiableAt 𝕜 f x v

Premises used: LineDifferentiableAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
H : LineDifferentiableAt 𝕜 f x v
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v

Tactic:
(H.hasLineDerivAt.smul c).lineDeriv

Premises used: HasLineDerivAt.lineDeriv, LineDifferentiableAt.hasLineDerivAt, HasLineDerivAt.smul
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
H : LineDifferentiableAt 𝕜 f x v
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v

Tactic:
exact (H.hasLineDerivAt.smul c).lineDeriv

Premises used: HasLineDerivAt.lineDeriv, LineDifferentiableAt.hasLineDerivAt, HasLineDerivAt.smul
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
H : ¬LineDifferentiableAt 𝕜 f x v
⊢ ¬LineDifferentiableAt 𝕜 f x (c • v)

Tactic:
simpa [lineDifferentiableAt_smul_iff hc] using H

Premises used: lineDifferentiableAt_smul_iff
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
H : ¬LineDifferentiableAt 𝕜 f x v
⊢ ¬LineDifferentiableAt 𝕜 f x (c • v)

Tactic:
have H' : ¬ (LineDifferentiableAt 𝕜 f x (c • v)) := by
      simpa [lineDifferentiableAt_smul_iff hc] using H
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
c : 𝕜
hc : c ≠ 0
H : ¬LineDifferentiableAt 𝕜 f x v
H' : ¬LineDifferentiableAt 𝕜 f x (c • v)
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v

Tactic:
simp [lineDeriv_zero_of_not_lineDifferentiableAt, H, H']

Premises used: lineDeriv_zero_of_not_lineDifferentiableAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
f : E → F
x v : E
rw : lineDeriv 𝕜 f x (HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (-1) v) = -lineDeriv 𝕜 f x v
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) (lineDeriv 𝕜 f x v) = -lineDeriv 𝕜 f x v
rw₂ rw₃ : -lineDeriv 𝕜 f x v = -lineDeriv 𝕜 f x v
⊢ lineDeriv 𝕜 f x (-v) = -lineDeriv 𝕜 f x v

Tactic:
rw [← neg_one_smul (R := 𝕜) v, lineDeriv_smul, neg_one_smul]

Premises used: neg_one_smul, lineDeriv_smul
-- 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
⊢ lieBracket 𝕜 V W = fun (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:
rfl

Premises used: VectorField.lieBracket, rfl
-- 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
⊢ lieBracketWithin 𝕜 V W s = 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)

Tactic:
rfl

Premises used: VectorField.lieBracketWithin, rfl
-- 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
h : ∀ (x : E), lieBracketWithin 𝕜 V W univ x = lieBracket 𝕜 V W x
⊢ lieBracketWithin 𝕜 V W univ = lieBracket 𝕜 V W

Tactic:
ext1 x
-- 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
⊢ lieBracketWithin 𝕜 V W univ x = lieBracket 𝕜 V W x

Tactic:
simp [lieBracketWithin, lieBracket]

Premises used: 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 : Set E
x : E
hV : V x = 0
hW : W x = 0
⊢ lieBracketWithin 𝕜 V W s x = 0

Tactic:
simp [lieBracketWithin, 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 : E → E
x : E
hV : V x = 0
hW : W x = 0
⊢ lieBracket 𝕜 V W x = 0

Tactic:
simp [lieBracket, hV, hW]

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

Tactic:
ext x
-- 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
⊢ lieBracketWithin 𝕜 V W s x = (-lieBracketWithin 𝕜 W V s) 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
V W : E → E
x : E
⊢ lieBracket 𝕜 V W x = -lieBracket 𝕜 W V x

Tactic:
simp [lieBracket]

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

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.VectorField
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V : E → E
s : Set E
x : E
⊢ lieBracketWithin 𝕜 V V 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
V : E → E
h : ∀ (x : E), lieBracket 𝕜 V V x = 0 x
⊢ lieBracket 𝕜 V V = 0

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

Tactic:
simp [lieBracket]

Premises used: 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 : Set E
x : E
c : 𝕜
hV : DifferentiableWithinAt 𝕜 V s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ lieBracketWithin 𝕜 (c • V) W s x = c • lieBracketWithin 𝕜 V W s x

Tactic:
simp [lieBracketWithin, smul_sub, fderivWithin_const_smul hs hV]

Premises used: smul_sub, fderivWithin_const_smul, 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
x : E
c : 𝕜
hV : DifferentiableAt 𝕜 V x
simp :
  ∀ (hV : DifferentiableWithinAt 𝕜 V univ x), lieBracketWithin 𝕜 (c • V) W univ x = c • lieBracketWithin 𝕜 V W univ x
⊢ lieBracket 𝕜 (c • V) W x = c • lieBracket 𝕜 V W x

Tactic:
simp only [← differentiableWithinAt_univ, ← lieBracketWithin_univ] at hV ⊢

Premises used: VectorField.lieBracketWithin_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
V W : E → E
x : E
c : 𝕜
hV : DifferentiableWithinAt 𝕜 V univ x
⊢ lieBracketWithin 𝕜 (c • V) W univ x = c • lieBracketWithin 𝕜 V W univ x

Tactic:
lieBracketWithin_const_smul_left hV uniqueDiffWithinAt_univ

Premises used: uniqueDiffWithinAt_univ, VectorField.lieBracketWithin_const_smul_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
x : E
c : 𝕜
hV : DifferentiableWithinAt 𝕜 V univ x
⊢ lieBracketWithin 𝕜 (c • V) W univ x = c • lieBracketWithin 𝕜 V W univ x

Tactic:
exact lieBracketWithin_const_smul_left hV uniqueDiffWithinAt_univ

Premises used: uniqueDiffWithinAt_univ, VectorField.lieBracketWithin_const_smul_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 : Set E
x : E
c : 𝕜
hW : DifferentiableWithinAt 𝕜 W s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ lieBracketWithin 𝕜 V (c • W) s x = c • lieBracketWithin 𝕜 V W s x

Tactic:
simp [lieBracketWithin, smul_sub, fderivWithin_const_smul hs hW]

Premises used: smul_sub, fderivWithin_const_smul, 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
x : E
c : 𝕜
hW : DifferentiableAt 𝕜 W x
simp :
  ∀ (hW : DifferentiableWithinAt 𝕜 W univ x), lieBracketWithin 𝕜 V (c • W) univ x = c • lieBracketWithin 𝕜 V W univ x
⊢ lieBracket 𝕜 V (c • W) x = c • lieBracket 𝕜 V W x

Tactic:
simp only [← differentiableWithinAt_univ, ← lieBracketWithin_univ] at hW ⊢

Premises used: VectorField.lieBracketWithin_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
V W : E → E
x : E
c : 𝕜
hW : DifferentiableWithinAt 𝕜 W univ x
⊢ lieBracketWithin 𝕜 V (c • W) univ x = c • lieBracketWithin 𝕜 V W univ x

Tactic:
lieBracketWithin_const_smul_right hW uniqueDiffWithinAt_univ

Premises used: uniqueDiffWithinAt_univ, VectorField.lieBracketWithin_const_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
c : 𝕜
hW : DifferentiableWithinAt 𝕜 W univ x
⊢ lieBracketWithin 𝕜 V (c • W) univ x = c • lieBracketWithin 𝕜 V W univ x

Tactic:
exact lieBracketWithin_const_smul_right hW uniqueDiffWithinAt_univ

Premises used: uniqueDiffWithinAt_univ, VectorField.lieBracketWithin_const_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
s : Set E
x : E
f : E → 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hW : DifferentiableWithinAt 𝕜 W s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ lieBracketWithin 𝕜 V (fun (y : E) ↦ f y • W y) s x =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (((fderivWithin 𝕜 f s x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (V x) : 𝕜) (W x) +
      f x • lieBracketWithin 𝕜 V W s x

Tactic:
simp [lieBracketWithin, fderivWithin_fun_smul hs hf hW, map_smul, add_comm, smul_sub,
    add_sub_assoc]

Premises used: add_sub_assoc, fderivWithin_fun_smul, add_comm, smul_sub, VectorField.lieBracketWithin, map_smul
-- 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
hW : DifferentiableAt 𝕜 W x
simp_rw :
  ∀ (hW : DifferentiableWithinAt 𝕜 W univ x) (hf : DifferentiableWithinAt 𝕜 f univ x),
    lieBracketWithin 𝕜 V (fun (y : E) ↦ f y • W y) univ x =
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (((fderivWithin 𝕜 f univ x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (V x) : 𝕜) (W x) +
        f x • lieBracketWithin 𝕜 V W univ x
⊢ lieBracket 𝕜 V (fun (y : E) ↦ f y • W y) x =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (((fderiv 𝕜 f x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (V x) : 𝕜) (W x) +
      f x • lieBracket 𝕜 V W x

Tactic:
simp_rw [← differentiableWithinAt_univ, ← lieBracketWithin_univ, fderiv] at hW hf ⊢

Premises used: VectorField.lieBracketWithin_univ, fderiv, 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
V W : E → E
x : E
f : E → 𝕜
hW : DifferentiableWithinAt 𝕜 W univ x
hf : DifferentiableWithinAt 𝕜 f univ x
⊢ lieBracketWithin 𝕜 V (fun (y : E) ↦ f y • W y) univ x =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (((fderivWithin 𝕜 f univ x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (V x) : 𝕜) (W x) +
      f x • lieBracketWithin 𝕜 V W univ x

Tactic:
lieBracketWithin_smul_right hf hW uniqueDiffWithinAt_univ

Premises used: uniqueDiffWithinAt_univ, VectorField.lieBracketWithin_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 → 𝕜
hW : DifferentiableWithinAt 𝕜 W univ x
hf : DifferentiableWithinAt 𝕜 f univ x
⊢ lieBracketWithin 𝕜 V (fun (y : E) ↦ f y • W y) univ x =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (((fderivWithin 𝕜 f univ x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (V x) : 𝕜) (W x) +
      f x • lieBracketWithin 𝕜 V W univ x

Tactic:
exact lieBracketWithin_smul_right hf hW uniqueDiffWithinAt_univ

Premises used: uniqueDiffWithinAt_univ, VectorField.lieBracketWithin_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
s : Set E
x : E
f : E → 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hV : DifferentiableWithinAt 𝕜 V s x
hs : UniqueDiffWithinAt 𝕜 s x
rw :
  -(f x • (-lieBracketWithin 𝕜 V W s) x +
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (((fderivWithin 𝕜 f s x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (W x) : 𝕜) (V x)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-((fderivWithin 𝕜 f s x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (W x) : 𝕜) (V x) +
      f x • lieBracketWithin 𝕜 V W s x
⊢ lieBracketWithin 𝕜 (fun (y : E) ↦ f y • V y) W s x =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-((fderivWithin 𝕜 f s x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (W x) : 𝕜) (V x) +
      f x • lieBracketWithin 𝕜 V W s x

Tactic:
rw [lieBracketWithin_swap, Pi.neg_apply, lieBracketWithin_smul_right hf hV hs,
    lieBracketWithin_swap, add_comm]

Premises used: add_comm, VectorField.lieBracketWithin_smul_right, VectorField.lieBracketWithin_swap, Pi.neg_apply
-- 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
f : E → 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hV : DifferentiableWithinAt 𝕜 V s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ -(f x • (-lieBracketWithin 𝕜 V W s) x +
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (((fderivWithin 𝕜 f s x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (W x) : 𝕜) (V x)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-((fderivWithin 𝕜 f s x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) (W x) : 𝕜) (V x) +
      f x • lieBracketWithin 𝕜 V W s x

Tactic:
simp