awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v
this : ∀ᶠ (x : E) in 𝓝 (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖x - 0‖
have h : ∀ (t : 𝕜)
  (ht :
    Membership.mem (γ := Set 𝕜)
      (preimage.{u_1, u_3} (β := E) (fun (t : 𝕜) ↦ x₀ + t • v) {x : E | ‖f x - f x₀‖ ≤ C * ‖x - x₀‖}) t),
  ‖f (x₀ + t • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖t - 0‖
Tactic: filter_upwards [(A.continuousAt (x := 0)).preimage_mem_nhds this] with t ht
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v
this : ∀ᶠ (x : E) in 𝓝 (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
t : 𝕜
ht :
  Membership.mem (γ := Set 𝕜)
    (preimage.{u_1, u_3} (β := E) (fun (t : 𝕜) ↦ x₀ + t • v) {x : E | ‖f x - f x₀‖ ≤ C * ‖x - x₀‖}) t
⊢ ‖f (x₀ + t • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖t - 0‖
have ht₁ : ‖f (x₀ + t • v) - f x₀‖ ≤ C * (‖v‖ * ‖t‖)
Tactic: simp only [preimage_setOf_eq, add_sub_cancel_left, norm_smul, mem_setOf_eq, mul_comm (‖t‖)] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖lineDeriv 𝕜 f x₀ v‖ ≤ (↑C : ℝ) * ‖v‖
have refine : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
Tactic: refine norm_lineDeriv_le_of_lip' 𝕜 C.coe_nonneg ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
have h : ∀ (a : E),
  Membership.mem (γ := Set E)
    {x : E | x ∈ s → Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖) x} x} a
Tactic: filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E | x ∈ s → Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖) x} x} a
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
have h₁ : ∀ a ∈ s, ‖f a - f x₀‖ ≤ (↑C : ℝ) * ‖a - x₀‖
Tactic: filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
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
⊢ HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • c • v)) (c • f') ((fun (t : 𝕜) ↦ x + t • c • v) ⁻¹' s) 0
have A : HasDerivAt g c 0
Tactic: have A : HasDerivAt g c 0 := by simpa using (hasDerivAt_id (0 : 𝕜)).const_smul c
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
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
⊢ HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • c • v)) (c • f') ((fun (t : 𝕜) ↦ x + t • c • v) ⁻¹' s) 0
have B : HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • v)) f' s' (g 0)
Tactic: have B : HasDerivWithinAt (fun t ↦ f (x + t • v)) f' s' (g 0) := by simpa [g] using h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
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)
⊢ HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • c • v)) (c • f') ((fun (t : 𝕜) ↦ x + t • c • v) ⁻¹' s) 0
have Z : HasDerivWithinAt ((fun (t : 𝕜) ↦ f (x + t • v)) ∘ g) (c • f') (g ⁻¹' s') 0
Tactic: have Z := B.scomp (0 : 𝕜) A.hasDerivWithinAt (mapsTo_preimage g s')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
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 (t : 𝕜) ↦ f (x + t • v)) ∘ g) (c • f') (g ⁻¹' s') 0
⊢ HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • c • v)) (c • f') ((fun (t : 𝕜) ↦ x + t • c • v) ⁻¹' s) 0
have 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
Tactic: simp only [g, s', Function.comp_def, smul_eq_mul, mul_comm c, ← smul_smul] at Z
Cleared hypotheses: Z
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
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
⊢ HasDerivWithinAt (fun (t : 𝕜) ↦ f (x + t • c • v)) (c • f') ((fun (t : 𝕜) ↦ x + t • c • v) ⁻¹' s) 0
have h₁ : Eq.{u_1 + 1} (α := Set 𝕜) ((fun (t : 𝕜) ↦ x + t • c • v) ⁻¹' s)
  (preimage (β := 𝕜) (fun (t : 𝕜) ↦ t * c) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s))
Tactic: convert! Z
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := Set 𝕜) ((fun (t : 𝕜) ↦ x + t • c • v) ⁻¹' s)
    (preimage (β := 𝕜) (fun (t : 𝕜) ↦ t * c) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s))
have 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
Tactic: ext t
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
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 : 𝕜
⊢ HasLineDerivAt 𝕜 f (c • f') x (c • v)
have simp : ∀ (h : HasLineDerivWithinAt 𝕜 f f' univ x v), HasLineDerivWithinAt 𝕜 f (c • f') univ x (c • v)
Tactic: simp only [← hasLineDerivWithinAt_univ] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
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 : 𝕜
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
have 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)
Tactic: rcases eq_or_ne c 0 with rfl | hc
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
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)
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
have inr : ∀ (hc : c ≠ 0), lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
Tactic: rcases eq_or_ne c 0 with rfl | hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
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
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
have pos : ∀ (H : LineDifferentiableAt 𝕜 f x v), lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
Tactic: by_cases H : LineDifferentiableAt 𝕜 f x v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
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
⊢ lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
have neg : ∀ (H : ¬LineDifferentiableAt 𝕜 f x v), lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
Tactic: by_cases H : LineDifferentiableAt 𝕜 f x v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
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
have H' : ¬LineDifferentiableAt 𝕜 f x (c • v)
Tactic: have H' : ¬ (LineDifferentiableAt 𝕜 f x (c • v)) := by
      simpa [lineDifferentiableAt_smul_iff hc] using H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
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 (-v) = -lineDeriv 𝕜 f x v
have rw : lineDeriv 𝕜 f x (HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (-1) v) = -lineDeriv 𝕜 f x v
Tactic: rw [← neg_one_smul (R := 𝕜) v, lineDeriv_smul, neg_one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
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
⊢ lineDeriv 𝕜 f x (-v) = -lineDeriv 𝕜 f x v
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) (lineDeriv 𝕜 f x v) = -lineDeriv 𝕜 f x v
Tactic: rw [← neg_one_smul (R := 𝕜) v, lineDeriv_smul, neg_one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
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
⊢ lineDeriv 𝕜 f x (-v) = -lineDeriv 𝕜 f x v
have rw₂ : -lineDeriv 𝕜 f x v = -lineDeriv 𝕜 f x v
Tactic: rw [← neg_one_smul (R := 𝕜) v, lineDeriv_smul, neg_one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W : E → E
⊢ lieBracketWithin 𝕜 V W univ = lieBracket 𝕜 V W
have h : ∀ (x : E), lieBracketWithin 𝕜 V W univ x = lieBracket 𝕜 V W x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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 = -lieBracketWithin 𝕜 W V s
have h : ∀ (x : E), lieBracketWithin 𝕜 V W s x = (-lieBracketWithin 𝕜 W V s) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V : E → E
s : Set E
⊢ lieBracketWithin 𝕜 V V s = 0
have h : ∀ (x : E), lieBracketWithin 𝕜 V V s x = 0 x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V : E → E
⊢ lieBracket 𝕜 V V = 0
have h : ∀ (x : E), lieBracket 𝕜 V V x = 0 x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ lieBracket 𝕜 (c • V) W x = c • lieBracket 𝕜 V W x
have simp : ∀ (hV : DifferentiableWithinAt 𝕜 V univ x), lieBracketWithin 𝕜 (c • V) W univ x = c • lieBracketWithin 𝕜 V W univ x
Tactic: simp only [← differentiableWithinAt_univ, ← lieBracketWithin_univ] at hV ⊢
Cleared hypotheses: hV
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ lieBracket 𝕜 V (c • W) x = c • lieBracket 𝕜 V W x
have simp : ∀ (hW : DifferentiableWithinAt 𝕜 W univ x), lieBracketWithin 𝕜 V (c • W) univ x = c • lieBracketWithin 𝕜 V W univ x
Tactic: simp only [← differentiableWithinAt_univ, ← lieBracketWithin_univ] at hW ⊢
Cleared hypotheses: hW
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ 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
have 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
Tactic: simp_rw [← differentiableWithinAt_univ, ← lieBracketWithin_univ, fderiv] at hW hf ⊢
Cleared hypotheses: hf, hW
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ 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
have 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
Tactic: rw [lieBracketWithin_swap, Pi.neg_apply, lieBracketWithin_smul_right hf hV hs,
    lieBracketWithin_swap, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ 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
have 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
Tactic: rw [lieBracket_swap, lieBracket_smul_right hf hV, lieBracket_swap, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ lieBracketWithin 𝕜 (V + V₁) W s x = lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V₁ W s x
have 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)
Tactic: simp only [lieBracketWithin, Pi.add_apply, map_add]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ 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)
have 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)
Tactic: rw [fderivWithin_add hs hV hV₁, ContinuousLinearMap.add_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ lieBracket 𝕜 (V + V₁) W x = lieBracket 𝕜 V W x + lieBracket 𝕜 V₁ W x
have 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)
Tactic: simp only [lieBracket, Pi.add_apply, map_add]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
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
⊢ 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)
have 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)
Tactic: rw [fderiv_add hV hV₁, ContinuousLinearMap.add_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
W : E → E
s : Set E
⊢ lieBracketWithin 𝕜 0 W s = 0
have h : ∀ (x : E), lieBracketWithin 𝕜 0 W s x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
W : E → E
s : Set E
⊢ lieBracketWithin 𝕜 W 0 s = 0
have h : ∀ (x : E), lieBracketWithin 𝕜 W 0 s x = 0 x
Tactic: ext