awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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
⊢ (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x

Tactic:
exact extChartAt_to_inv x

Premises used: extChartAt_to_inv
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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
e_1 : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)) = TangentSpace I x
⊢ (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x

Tactic:
extChartAt_to_inv x

Premises used: extChartAt_to_inv
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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
e_1 : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)) = TangentSpace I x
⊢ (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x

Tactic:
exact extChartAt_to_inv x

Premises used: extChartAt_to_inv
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 :
  {x_1 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) |
      (fun (x_2 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) ↦
          Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁ (range (↑I : H → E)) x_2 :
              TangentSpace 𝓘(𝕜, E) x_2)
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)) x_2))
        x_1} ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x
⊢ 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 nhdsWithin_mono _ inter_subset_left

Premises used: Set.inter_subset_left, nhdsWithin_mono
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 :
  ∀ (y : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    (hy :
      y ∈ (↑(extChartAt I x).symm : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) → M) ⁻¹' {x : M | W₁ x = W x}),
    Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁ (range (↑I : H → E)) y : TangentSpace 𝓘(𝕜, E) y)
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)) y)
⊢ {x_1 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) |
      (fun (x_2 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) ↦
          Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁ (range (↑I : H → E)) x_2 :
              TangentSpace 𝓘(𝕜, E) x_2)
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)) x_2))
        x_1} ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x

Tactic:
filter_upwards [(continuousAt_extChartAt_symm x).continuousWithinAt.preimage_mem_nhdsWithin''
      hW (by simp)] with y hy

Premises used: ContinuousAt.continuousWithinAt, ContinuousWithinAt.preimage_mem_nhdsWithin'', continuousAt_extChartAt_symm
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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
y : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)
hy : y ∈ (↑(extChartAt I x).symm : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) → M) ⁻¹' {x : M | W₁ x = W x}
⊢ Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    ((ContinuousLinearMap.inverse (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) :
        (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) y)) → TangentSpace 𝓘(𝕜, E) y)
      (W₁ ((↑(extChartAt I x).symm : E → M) y)))
    ((ContinuousLinearMap.inverse (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) :
        (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) y)) → TangentSpace 𝓘(𝕜, E) y)
      (W ((↑(extChartAt I x).symm : E → M) y)))

Tactic:
congr 1
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 :
  Eq.{u_3 + 1} (α := TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (W₁ ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (W ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
⊢ Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    ((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))))
    ((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))))

Tactic:
congr 1
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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
⊢ W₁ x = W x

Tactic:
hxW
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x
h₁ h₂ :
  TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)) = TangentSpace I x →
    (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x
⊢ Eq.{u_3 + 1} (α := TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (W₁ ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (W ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))

Tactic:
convert! hxW
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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
hW : W₁ =ᶠ[𝓝[s] x] W
hx : x ∈ s
⊢ mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x

Tactic:
hV.mlieBracketWithin_vectorField_eq (mem_of_mem_nhdsWithin hx hV :)
    hW (mem_of_mem_nhdsWithin hx hW :)

Premises used: mem_of_mem_nhdsWithin, Filter.EventuallyEq.mlieBracketWithin_vectorField_eq
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
h :
  ∀ (y : M) (hVy : V₁ y = V y) (hWy : W₁ y = W y) (hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x)
    (hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x), mlieBracketWithin I V₁ W₁ t y = mlieBracketWithin I V W t y
⊢ mlieBracketWithin I V₁ W₁ t =ᶠ[𝓝[s] x] mlieBracketWithin I V W t

Tactic:
filter_upwards [hV, hW, eventually_eventually_nhdsWithin.2 hV,
    eventually_eventually_nhdsWithin.2 hW] with y hVy hWy hVy' hWy'

Premises used: Iff.mpr, eventually_eventually_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
h : V₁ =ᶠ[𝓝[t] y] V
h₁ : V₁ y = V y
h₂ : W₁ =ᶠ[𝓝[t] y] W
h₃ : W₁ y = W y
⊢ mlieBracketWithin I V₁ W₁ t y = mlieBracketWithin I V W t y

Tactic:
apply Filter.EventuallyEq.mlieBracketWithin_vectorField_eq

Premises used: Filter.EventuallyEq.mlieBracketWithin_vectorField_eq
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
h : {x : M | (fun (x : M) ↦ V₁ x = V x) x} ∈ 𝓝[s] y
⊢ V₁ =ᶠ[𝓝[t] y] V

Tactic:
apply nhdsWithin_mono _ ht

Premises used: nhdsWithin_mono
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ {x : M | (fun (x : M) ↦ V₁ x = V x) x} ∈ 𝓝[s] y

Tactic:
hVy'

Premises used: Filter.Eventually
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ {x : M | (fun (x : M) ↦ V₁ x = V x) x} ∈ 𝓝[s] y

Tactic:
exact hVy'
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ V₁ y = V y

Tactic:
hVy

Premises used: TangentSpace
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ V₁ y = V y

Tactic:
exact hVy
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
h : {x : M | (fun (x : M) ↦ W₁ x = W x) x} ∈ 𝓝[s] y
⊢ W₁ =ᶠ[𝓝[t] y] W

Tactic:
apply nhdsWithin_mono _ ht

Premises used: nhdsWithin_mono
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ {x : M | (fun (x : M) ↦ W₁ x = W x) x} ∈ 𝓝[s] y

Tactic:
hWy'

Premises used: Filter.Eventually
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ {x : M | (fun (x : M) ↦ W₁ x = W x) x} ∈ 𝓝[s] y

Tactic:
exact hWy'
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ W₁ y = W y

Tactic:
hWy

Premises used: TangentSpace
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ W₁ y = W y

Tactic:
exact hWy
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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
hW : W₁ =ᶠ[𝓝[s] x] W
⊢ mlieBracketWithin I V₁ W₁ s =ᶠ[𝓝[s] x] mlieBracketWithin I V W s

Tactic:
hV.mlieBracketWithin_vectorField' hW Subset.rfl

Premises used: Filter.EventuallyEq.mlieBracketWithin_vectorField', Set.Subset.rfl
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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₁ =ᶠ[𝓝[insert x s] x] V
hW : W₁ =ᶠ[𝓝[insert x s] x] W
⊢ mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x

Tactic:
apply mem_of_mem_nhdsWithin (mem_insert x s)
    (hV.mlieBracketWithin_vectorField' hW (subset_insert x s))

Premises used: Filter.EventuallyEq.mlieBracketWithin_vectorField', mem_of_mem_nhdsWithin, Set.mem_insert, Set.subset_insert
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
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₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
⊢ mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x

Tactic:
(hV.filter_mono nhdsWithin_le_nhds).mlieBracketWithin_vectorField_eq hV.self_of_nhds
    (hW.filter_mono nhdsWithin_le_nhds) hW.self_of_nhds

Premises used: Filter.EventuallyEq.filter_mono, Filter.Eventually.self_of_nhds, nhdsWithin_le_nhds, Filter.EventuallyEq.mlieBracketWithin_vectorField_eq