awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
this : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x
⊢ Eq (α := E)
    ((ContinuousLinearMap.inverse
            (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
              ((↑(extChartAt I x) : M → E) x)) :
          (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) →
            TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
        (W ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) :
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    0
have hW₁ : Eq (α := E)
  (((ContinuousLinearMap.inverse
            (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
              ((↑(extChartAt I x) : M → E) x)) :
          TangentSpace I x →L[𝕜] TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :
        (a : TangentSpace I x) → TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
      0 :
    TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
  0
Tactic: rw [this, hW]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
⊢ mlieBracketWithin I V W s x = -mlieBracketWithin I W V s x
have rw : (-mpullback I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E)
        (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))))
    x =
  -mlieBracketWithin I W V s x
Tactic: rw [mlieBracketWithin, lieBracketWithin_swap, mpullback_neg]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
V W : (x : M) → TangentSpace I x
⊢ mlieBracketWithin I V W s = -mlieBracketWithin I W V s
have h : ∀ (x : M), mlieBracketWithin I V W s x = (-mlieBracketWithin I W V s) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
V : (x : M) → TangentSpace I x
⊢ mlieBracketWithin I V V = 0
have h : ∀ (x : Set M) (x_1 : M), mlieBracketWithin I V V x x_1 = 0 x x_1
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
V : (x : M) → TangentSpace I x
⊢ mlieBracket I V V = 0
have h : ∀ (x : M), mlieBracket I V V x = 0 x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
V : (x : M) → TangentSpace I x
x : M
⊢ mlieBracket I V V x = 0 x
have h : mlieBracketWithin I V V univ x = 0 x
Tactic: simp_rw [mlieBracket, mlieBracketWithin_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
V : (x : M) → TangentSpace I x
x : M
h : mlieBracketWithin I V V univ x = 0 x
⊢ mlieBracket I V V x = 0 x
have h₁ : Eq.{u_3 + 1} (α := TangentSpace I x) (0 univ x) (0 x)
Tactic: simp_rw [mlieBracket, mlieBracketWithin_self, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
W : (x : M) → TangentSpace I x
⊢ mlieBracketWithin I 0 W s = 0
have h : ∀ (x : M), mlieBracketWithin I 0 W s x = 0 x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
W : (x : M) → TangentSpace I x
⊢ mlieBracketWithin I W 0 s = 0
have rw : -mlieBracketWithin I 0 W s = 0
Tactic: rw [mlieBracketWithin_swap]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ Eq (α := TangentSpace I x)
    ((ContinuousLinearMap.inverse (mfderiv% (↑(extChartAt I x) : M → E) x) :
          (a : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) → TangentSpace I x)
        (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)) :
      TangentSpace I x)
    ((ContinuousLinearMap.inverse (mfderiv% (↑(extChartAt I x) : M → E) x) :
          (a : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) → TangentSpace I x)
        (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)) :
      TangentSpace I x)
have h₁ : lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) =
  lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) =
    lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have h₁ : (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝[≠] (↑(extChartAt I x) : M → E) x]
  (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
Tactic: suffices A : ((extChartAt I x).symm ⁻¹' s ∩ range I : Set E)
    =ᶠ[𝓝[{(extChartAt I x) x}ᶜ] (extChartAt I x x)]
      ((extChartAt I x).symm ⁻¹' t ∩ range I : Set E) by
    apply lieBracketWithin_congr_set' _ A
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
ht : t ∈ 𝓝 x
⊢ mlieBracketWithin I V W (s ∩ t) x = mlieBracketWithin I V W s x
have h : s ∩ t =ᶠ[𝓝 x] s
Tactic: apply mlieBracketWithin_congr_set
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
ht : t ∈ 𝓝 x
⊢ s ∩ t =ᶠ[𝓝 x] s
have h : ∀ (y : M) (hy : y ∈ t), (s ∩ t) y = s y
Tactic: filter_upwards [ht] with y hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
ht : t ∈ 𝓝 x
y : M
hy : y ∈ t
⊢ (s ∩ t) y = s y
have h : (y ∈ s ∩ t) = (y ∈ s)
Tactic: change (y ∈ s ∩ t) = (y ∈ s)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
h : s ∈ 𝓝 x
⊢ mlieBracketWithin I V W s x = mlieBracket I V W x
have rw : mlieBracketWithin I V W s x = mlieBracketWithin I V W univ x
Tactic: rw [← mlieBracketWithin_univ, ← univ_inter s, mlieBracketWithin_inter h]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
h : s ∈ 𝓝 x
rw : mlieBracketWithin I V W s x = mlieBracketWithin I V W univ x
⊢ mlieBracketWithin I V W s x = mlieBracket I V W x
have rw₁ : mlieBracketWithin I V W (univ ∩ s) x = mlieBracketWithin I V W univ x
Tactic: rw [← mlieBracketWithin_univ, ← univ_inter s, mlieBracketWithin_inter h]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
h : s ∈ 𝓝 x
rw : mlieBracketWithin I V W s x = mlieBracketWithin I V W univ x
rw₁ : mlieBracketWithin I V W (univ ∩ s) x = mlieBracketWithin I V W univ x
⊢ mlieBracketWithin I V W s x = mlieBracket I V W x
have rw₂ : mlieBracketWithin I V W univ x = mlieBracketWithin I V W univ x
Tactic: rw [← mlieBracketWithin_univ, ← univ_inter s, mlieBracketWithin_inter h]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
⊢ Eq (α := TangentSpace I x)
    ((ContinuousLinearMap.inverse (mfderiv% (↑(extChartAt I x) : M → E) x) :
          (a : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) → TangentSpace I x)
        (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁ (range (↑I : H → E)))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)) :
      TangentSpace I x)
    ((ContinuousLinearMap.inverse (mfderiv% (↑(extChartAt I x) : M → E) x) :
          (a : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) → TangentSpace I x)
        (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)) :
      TangentSpace I x)
have h : lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)))
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁ (range (↑I : H → E)))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) =
  lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
⊢ lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁ (range (↑I : H → E)))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) =
    lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have h : mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁
    (range
      (↑I : H → E)) =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))
Tactic: apply Filter.EventuallyEq.lieBracketWithin_vectorField_eq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
h :
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁
      (range
        (↑I : H → E)) =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))
⊢ lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁ (range (↑I : H → E)))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) =
    lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have h₁ : Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
  (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
  (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
Tactic: apply Filter.EventuallyEq.lieBracketWithin_vectorField_eq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
h :
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁
      (range
        (↑I : H → E)) =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))
h₁ :
  Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
⊢ lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁ (range (↑I : H → E)))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) =
    lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have h₂ : mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁
    (range
      (↑I : H → E)) =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E))
Tactic: apply Filter.EventuallyEq.lieBracketWithin_vectorField_eq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorField.LieBracket (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
h :
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁
      (range
        (↑I : H → E)) =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))
h₁ :
  Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
h₂ :
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁
      (range
        (↑I : H → E)) =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E))
⊢ lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁ (range (↑I : H → E)))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) =
    lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have h₃ : Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
  (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁ (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
  (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
Tactic: apply Filter.EventuallyEq.lieBracketWithin_vectorField_eq