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
V W : (x : M) → TangentSpace I x
⊢ mlieBracketWithin I V W s = fun (x₀ : M) ↦
    mpullback I 𝓘(𝕜, E) (↑(extChartAt I x₀) : M → 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)))
      x₀

Tactic:
rfl

Premises used: VectorField.mlieBracketWithin, 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 : (x : M) → TangentSpace I x
⊢ mlieBracketWithin I V W s 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₀))

Tactic:
rfl

Premises used: VectorField.mlieBracketWithin, VectorField.mpullback, rfl
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
h : ∀ (x : E), mlieBracketWithin 𝓘(𝕜, E) V W s x = lieBracketWithin 𝕜 V W s x
⊢ mlieBracketWithin 𝓘(𝕜, E) V W s = lieBracketWithin 𝕜 V W s

Tactic:
ext x
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
V W : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
⊢ mlieBracketWithin 𝓘(𝕜, E) V W s x = lieBracketWithin 𝕜 V W s x

Tactic:
simp [mlieBracketWithin_apply]

Premises used: VectorField.mlieBracketWithin_apply
-- 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
V W : (x : M) → TangentSpace I x
⊢ mlieBracketWithin I V W univ = mlieBracket I V W

Tactic:
rfl

Premises used: VectorField.mlieBracket, 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
rw :
  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)
        0 :
      TangentSpace I x)
    (0 : TangentSpace I x)
hV₁ :
  Eq (α := E)
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) :
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    0
hW₁ :
  Eq (α := E)
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) :
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    0
⊢ 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)
    (0 : TangentSpace I x)

Tactic:
rw [lieBracketWithin_eq_zero_of_eq_zero]

Premises used: VectorField.lieBracketWithin_eq_zero_of_eq_zero
-- 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ 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)
        0 :
      TangentSpace I x)
    (0 : TangentSpace I x)

Tactic:
simp
-- 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x

Tactic:
simp
-- 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 : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x

Tactic:
have : (extChartAt I x).symm ((extChartAt I x) x) = x := by simp
-- 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 : (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
hV₁ :
  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
⊢ 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))
        (V ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) :
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    0

Tactic:
rw [this, hV]
-- 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 : (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)) :
            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:
simp +instances
-- 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 : (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
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
⊢ 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

Tactic:
rw [this, hW]
-- 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 : (x : M) → TangentSpace I x
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
⊢ mlieBracketWithin I V W s x = -mlieBracketWithin I W V s x

Tactic:
rw [mlieBracketWithin, lieBracketWithin_swap, mpullback_neg]

Premises used: VectorField.mlieBracketWithin, VectorField.lieBracketWithin_swap, VectorField.mpullback_neg
-- 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 : (x : M) → TangentSpace I x
⊢ (-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:
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
V W : (x : M) → TangentSpace I x
h : ∀ (x : M), mlieBracketWithin I V W s x = (-mlieBracketWithin I W V s) x
⊢ mlieBracketWithin I V W s = -mlieBracketWithin I W V s

Tactic:
ext x
-- 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
V W : (x : M) → TangentSpace I x
x : M
⊢ mlieBracketWithin I V W s x = (-mlieBracketWithin I W V s) x

Tactic:
mlieBracketWithin_swap_apply

Premises used: VectorField.mlieBracketWithin_swap_apply
-- 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
V W : (x : M) → TangentSpace I x
x : M
⊢ mlieBracketWithin I V W s x = (-mlieBracketWithin I W V s) x

Tactic:
exact mlieBracketWithin_swap_apply

Premises used: VectorField.mlieBracketWithin_swap_apply
-- 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
x : M
V W : (x : M) → TangentSpace I x
⊢ mlieBracket I V W x = -mlieBracket I W V x

Tactic:
mlieBracketWithin_swap_apply

Premises used: VectorField.mlieBracketWithin_swap_apply, VectorField.mlieBracket
-- 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
V W : (x : M) → TangentSpace I x
⊢ mlieBracket I V W = -mlieBracket I W V

Tactic:
mlieBracketWithin_swap

Premises used: VectorField.mlieBracket, VectorField.mlieBracketWithin_swap
-- 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
V : (x : M) → TangentSpace I x
h : ∀ (x : Set M) (x_1 : M), mlieBracketWithin I V V x x_1 = 0 x x_1
⊢ mlieBracketWithin I V V = 0

Tactic:
ext x
-- 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
V : (x : M) → TangentSpace I x
x : Set M
x_1 : M
⊢ mlieBracketWithin I V V x x_1 = 0 x x_1

Tactic:
simp [mlieBracketWithin, mpullback]

Premises used: VectorField.mlieBracketWithin, VectorField.mpullback
-- 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
V : (x : M) → TangentSpace I x
h : ∀ (x : M), mlieBracket I V V x = 0 x
⊢ mlieBracket I V V = 0

Tactic:
ext x
-- 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
V : (x : M) → TangentSpace I x
x : M
h : mlieBracketWithin I V V univ x = 0 x
h₁ : Eq.{u_3 + 1} (α := TangentSpace I x) (0 univ x) (0 x)
⊢ mlieBracket I V V x = 0 x

Tactic:
simp_rw [mlieBracket, mlieBracketWithin_self, Pi.zero_apply]

Premises used: Pi.zero_apply, VectorField.mlieBracketWithin_self, VectorField.mlieBracket
-- 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
W : (x : M) → TangentSpace I x
h : ∀ (x : M), mlieBracketWithin I 0 W s x = 0 x
⊢ mlieBracketWithin I 0 W s = 0

Tactic:
ext x
-- 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
W : (x : M) → TangentSpace I x
x : M
⊢ mlieBracketWithin I 0 W s x = 0 x

Tactic:
simp [mlieBracketWithin]

Premises used: VectorField.mlieBracketWithin
-- 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
W : (x : M) → TangentSpace I x
rw : -mlieBracketWithin I 0 W s = 0
⊢ mlieBracketWithin I W 0 s = 0

Tactic:
rw [mlieBracketWithin_swap]

Premises used: VectorField.mlieBracketWithin_swap
-- 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
W : (x : M) → TangentSpace I x
⊢ -mlieBracketWithin I 0 W s = 0

Tactic:
simp
-- 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
W : (x : M) → TangentSpace I x
⊢ mlieBracket I 0 W = 0

Tactic:
simp [← mlieBracketWithin_univ]

Premises used: VectorField.mlieBracketWithin_univ
-- 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
W : (x : M) → TangentSpace I x
⊢ mlieBracket I W 0 = 0

Tactic:
simp [← mlieBracketWithin_univ]

Premises used: VectorField.mlieBracketWithin_univ
-- 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 : (x : M) → TangentSpace I x
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
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)
⊢ 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)

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 t : Set M
x : M
V W : (x : M) → TangentSpace I x
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
A :
  (↑(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)
⊢ 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:
apply lieBracketWithin_congr_set' _ A

Premises used: VectorField.lieBracketWithin_congr_set'
-- 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 : (x : M) → TangentSpace I x
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
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)
⊢ 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:
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