awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 W₁ : E → E
s : Set E
x : E
hW : DifferentiableWithinAt 𝕜 W s x
hW₁ : DifferentiableWithinAt 𝕜 W₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ lieBracketWithin 𝕜 V (W + W₁) s x = lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V W₁ s x
have 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)
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 W₁ : E → E
s : Set E
x : E
hW : DifferentiableWithinAt 𝕜 W s x
hW₁ : DifferentiableWithinAt 𝕜 W₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ 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)
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 hW hW₁, 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 W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
⊢ lieBracket 𝕜 V (W + W₁) x = lieBracket 𝕜 V W x + lieBracket 𝕜 V W₁ x
have 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)
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 W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
⊢ 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)
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 hW hW₁, ContinuousLinearMap.add_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (hypothesis)
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
⊢ (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)
have H₀ : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (hypothesis)
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
⊢ (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)
have H₁ : UniqueDiffWithinAt 𝕜 s x
Tactic: have H₁ : UniqueDiffWithinAt 𝕜 s x := hs x hxs
-- 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
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)
      ((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)
have 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)
Tactic: rw [fderivWithin_clm_apply, fderivWithin_clm_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
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
⊢ (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)
have 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)
Tactic: simp only [← fderivWithin_univ, ← lieBracketWithin_univ, ← contDiffWithinAt_univ,
    ← isSymmSndFDerivWithinAt_univ, ← differentiableWithinAt_univ] at *
Cleared hypotheses: hf, hsymm, hW, 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
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
⊢ (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)
have hf₁ : ContDiffWithinAt 𝕜 2 f s x
Tactic: apply fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt
-- 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
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
⊢ (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)
have hsymm : IsSymmSndFDerivWithinAt 𝕜 f s x
Tactic: apply fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt
-- 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
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
⊢ (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)
have hf₁ : ContDiffAt 𝕜 2 f x
Tactic: apply fderiv_apply_lieBracket_of_isSymmSndFDerivAt
-- 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
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
⊢ (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)
have hsymm : IsSymmSndFDerivAt 𝕜 f x
Tactic: apply fderiv_apply_lieBracket_of_isSymmSndFDerivAt
-- 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
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 𝕜 m (lieBracketWithin 𝕜 V W s) s x
have hf : ContDiffWithinAt 𝕜 (F := E) m (fun (x : E) ↦ (fderivWithin 𝕜 W s x : (a : E) → E) (V x)) s x
Tactic: apply ContDiffWithinAt.sub
-- 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
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
⊢ ContDiffWithinAt 𝕜 m (lieBracketWithin 𝕜 V W s) s x
have hg : ContDiffWithinAt 𝕜 (F := E) m (fun (x : E) ↦ (fderivWithin 𝕜 V s x : (a : E) → E) (W x)) s x
Tactic: apply ContDiffWithinAt.sub
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (hypothesis)
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
⊢ ContDiffAt 𝕜 m (lieBracket 𝕜 V W) x
have hV₁ : ContDiffWithinAt 𝕜 n V univ x
Tactic: rw [← contDiffWithinAt_univ] at hV hW ⊢
Cleared hypotheses: hV, hW, hmn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.VectorField (hypothesis)
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
⊢ ContDiffAt 𝕜 m (lieBracket 𝕜 V W) x
have hW₁ : ContDiffWithinAt 𝕜 n W univ x
Tactic: rw [← contDiffWithinAt_univ] at hV hW ⊢
Cleared hypotheses: hV, hW, hmn
-- 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
m n : ℕ∞ω
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
hmn : m + 1 ≤ n
⊢ ContDiffWithinAt 𝕜 m (lieBracket 𝕜 V W) univ x
have simp_rw : ContDiffWithinAt 𝕜 m (lieBracketWithin 𝕜 V W univ) univ x
Tactic: simp_rw [← lieBracketWithin_univ]
-- 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
h : s ∈ 𝓝 x
⊢ lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x
have rw : lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W univ x
Tactic: rw [← lieBracketWithin_univ, ← univ_inter s, lieBracketWithin_inter h]
-- 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
h : s ∈ 𝓝 x
rw : lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W univ x
⊢ lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x
have rw₁ : lieBracketWithin 𝕜 V W (univ ∩ s) x = lieBracketWithin 𝕜 V W univ x
Tactic: rw [← lieBracketWithin_univ, ← univ_inter s, lieBracketWithin_inter h]
-- 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
h : s ∈ 𝓝 x
rw : lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W univ x
rw₁ : lieBracketWithin 𝕜 V W (univ ∩ s) x = lieBracketWithin 𝕜 V W univ x
⊢ lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x
have rw₂ : lieBracketWithin 𝕜 V W univ x = lieBracketWithin 𝕜 V W univ x
Tactic: rw [← lieBracketWithin_univ, ← univ_inter s, lieBracketWithin_inter h]
-- 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₁ W₁ : E → E
s t : Set E
x : E
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
⊢ lieBracketWithin 𝕜 V₁ W₁ t =ᶠ[𝓝[s] x] lieBracketWithin 𝕜 V W t
have h : ∀ (x : E) (hV' : Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 V₁ t x) (fderivWithin 𝕜 V t x))
  (hW' : Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 W₁ t x) (fderivWithin 𝕜 W t x)) (hV : V₁ x = V x) (hW : W₁ x = W x),
  lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W t x
Tactic: filter_upwards [hV.fderivWithin' ht (𝕜 := 𝕜), hW.fderivWithin' ht (𝕜 := 𝕜), hV, hW]
    with x hV' hW' hV 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 V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
⊢ lieBracket 𝕜 V₁ W₁ x = lieBracket 𝕜 V W x
have rw : lieBracketWithin 𝕜 V₁ W₁ univ x = lieBracket 𝕜 V W x
Tactic: rw [← lieBracketWithin_univ, ← lieBracketWithin_univ, hV.lieBracketWithin_vectorField_eq_nhds 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 V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
rw : lieBracketWithin 𝕜 V₁ W₁ univ x = lieBracket 𝕜 V W x
⊢ lieBracket 𝕜 V₁ W₁ x = lieBracket 𝕜 V W x
have rw₁ : lieBracketWithin 𝕜 V₁ W₁ univ x = lieBracketWithin 𝕜 V W univ x
Tactic: rw [← lieBracketWithin_univ, ← lieBracketWithin_univ, hV.lieBracketWithin_vectorField_eq_nhds 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 V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
rw : lieBracketWithin 𝕜 V₁ W₁ univ x = lieBracket 𝕜 V W x
rw₁ : lieBracketWithin 𝕜 V₁ W₁ univ x = lieBracketWithin 𝕜 V W univ x
⊢ lieBracket 𝕜 V₁ W₁ x = lieBracket 𝕜 V W x
have rw₂ : lieBracketWithin 𝕜 V W univ x = lieBracketWithin 𝕜 V W univ x
Tactic: rw [← lieBracketWithin_univ, ← lieBracketWithin_univ, hV.lieBracketWithin_vectorField_eq_nhds 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 V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
⊢ lieBracket 𝕜 V₁ W₁ =ᶠ[𝓝 x] lieBracket 𝕜 V W
have h : ∀ (y : E) (hVy : V₁ =ᶠ[𝓝 y] V) (hWy : W₁ =ᶠ[𝓝 y] W), lieBracket 𝕜 V₁ W₁ y = lieBracket 𝕜 V W y
Tactic: filter_upwards [hV.eventuallyEq_nhds, hW.eventuallyEq_nhds] with y hVy hWy
-- 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
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 2 U s x
hV : ContDiffWithinAt 𝕜 2 V s x
hW : ContDiffWithinAt 𝕜 2 W s x
h'U : IsSymmSndFDerivWithinAt 𝕜 U s x
h'V : IsSymmSndFDerivWithinAt 𝕜 V s x
h'W : IsSymmSndFDerivWithinAt 𝕜 W s x
⊢ lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W s) s x =
    lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V s) W s x + lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W s) s x
have simp : HSub.hSub (α := E)
    ((fderivWithin 𝕜
            (fun (x : E) ↦
              HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V x) : E)
                ((fderivWithin 𝕜 V s x : (a : E) → E) (W x) : E))
            s x :
          (a : E) → E)
        (U x) :
      E)
    (HSub.hSub (α := E) (β := E)
      ((fderivWithin 𝕜 U s x : (a : E) → E) ((fderivWithin 𝕜 W s x : (a : E) → E) (V x) : E) : E)
      ((fderivWithin 𝕜 U s x : (a : E) → E) ((fderivWithin 𝕜 V s x : (a : E) → E) (W x) : E) : E)) =
  HSub.hSub (β := E)
      (HSub.hSub (α := E) (β := E)
        ((fderivWithin 𝕜 W s x : (a : E) → E) ((fderivWithin 𝕜 V s x : (a : E) → E) (U x) : E) : E)
        ((fderivWithin 𝕜 W s x : (a : E) → E) ((fderivWithin 𝕜 U s x : (a : E) → E) (V x) : E) : E))
      ((fderivWithin 𝕜
              (fun (x : E) ↦
                HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 V s x : (a : E) → E) (U x) : E)
                  ((fderivWithin 𝕜 U s x : (a : E) → E) (V x) : E))
              s x :
            (a : E) → E)
          (W x) :
        E) +
    HSub.hSub (α := E)
      ((fderivWithin 𝕜
              (fun (x : E) ↦
                HSub.hSub (α := E) (β := E) ((fderivWithin 𝕜 W s x : (a : E) → E) (U x) : E)
                  ((fderivWithin 𝕜 U s x : (a : E) → E) (W x) : E))
              s x :
            (a : E) → E)
          (V x) :
        E)
      (HSub.hSub (α := E) (β := E)
        ((fderivWithin 𝕜 V s x : (a : E) → E) ((fderivWithin 𝕜 W s x : (a : E) → E) (U x) : E) : E)
        ((fderivWithin 𝕜 V s x : (a : E) → E) ((fderivWithin 𝕜 U s x : (a : E) → E) (W x) : E) : E))
Tactic: simp only [lieBracketWithin_eq, map_sub]