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 : (x : M) → TangentSpace I x
c : 𝕜
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hW : MDiffAt[s] (T% W) x
hs : UniqueMDiffWithinAt I s x
⊢ mlieBracketWithin I V (c • W) s x = c • mlieBracketWithin I V W s x

Tactic:
simpa [mfderivWithin_const] using
    mlieBracketWithin_smul_right (mdifferentiableWithinAt_const (c := c)) (V := V) hW hs

Premises used: mdifferentiableWithinAt_const, VectorField.mlieBracketWithin_smul_right, mfderivWithin_const
-- 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
c : 𝕜
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hW : MDiffAt (T% W) x
simp : mlieBracketWithin I V (c • W) univ x = c • mlieBracketWithin I V W univ x
⊢ mlieBracket I V (c • W) x = c • mlieBracket I V W x

Tactic:
simp only [← mlieBracketWithin_univ] at hW ⊢

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
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hW : MDiffAt (T% W) x
⊢ mlieBracketWithin I V (c • W) univ x = c • mlieBracketWithin I V W univ x

Tactic:
mlieBracketWithin_const_smul_right hW (uniqueMDiffWithinAt_univ _)

Premises used: VectorField.mlieBracketWithin_const_smul_right, uniqueMDiffWithinAt_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
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hW : MDiffAt (T% W) x
⊢ mlieBracketWithin I V (c • W) univ x = c • mlieBracketWithin I V W univ x

Tactic:
exact mlieBracketWithin_const_smul_right hW (uniqueMDiffWithinAt_univ _)

Premises used: VectorField.mlieBracketWithin_const_smul_right, uniqueMDiffWithinAt_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 : Set M
x : M
V W V₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hV₁ : MDiffAt[s] (T% V₁) x
hs : UniqueMDiffWithinAt I s x
simp :
  (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 + 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)) =
    HAdd.hAdd (α := TangentSpace I 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)
      ((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)
⊢ mlieBracketWithin I (V + V₁) W s x = mlieBracketWithin I V W s x + mlieBracketWithin I V₁ W s x

Tactic:
simp only [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
s : Set M
x : M
V W V₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hV₁ : MDiffAt[s] (T% V₁) x
hs : UniqueMDiffWithinAt I s x
hV₂ :
  DifferentiableWithinAt 𝕜 (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)
hV₃ :
  DifferentiableWithinAt 𝕜 (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)
hs₁ : UniqueDiffWithinAt 𝕜 ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) 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 + 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)) =
    HAdd.hAdd (α := TangentSpace I 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)
      ((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)

Tactic:
rw [← map_add, mpullbackWithin_add, lieBracketWithin_add_left]

Premises used: VectorField.mpullbackWithin_add, map_add, VectorField.lieBracketWithin_add_left
-- 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₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hV₁ : MDiffAt[s] (T% V₁) x
hs : UniqueMDiffWithinAt I s x
⊢ DifferentiableWithinAt 𝕜 (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)

Tactic:
hV.differentiableWithinAt_mpullbackWithin_vectorField

Premises used: MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField
-- 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₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hV₁ : MDiffAt[s] (T% V₁) x
hs : UniqueMDiffWithinAt I s x
⊢ DifferentiableWithinAt 𝕜 (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)

Tactic:
exact hV.differentiableWithinAt_mpullbackWithin_vectorField

Premises used: MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField
-- 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₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hV₁ : MDiffAt[s] (T% V₁) x
hs : UniqueMDiffWithinAt I s x
⊢ DifferentiableWithinAt 𝕜 (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)

Tactic:
hV₁.differentiableWithinAt_mpullbackWithin_vectorField

Premises used: MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField
-- 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₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hV₁ : MDiffAt[s] (T% V₁) x
hs : UniqueMDiffWithinAt I s x
⊢ DifferentiableWithinAt 𝕜 (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)

Tactic:
exact hV₁.differentiableWithinAt_mpullbackWithin_vectorField

Premises used: MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField
-- 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₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hV₁ : MDiffAt[s] (T% V₁) x
hs : UniqueMDiffWithinAt I s x
⊢ UniqueDiffWithinAt 𝕜 ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
uniqueMDiffWithinAt_iff_inter_range.1 hs

Premises used: uniqueMDiffWithinAt_iff_inter_range, Iff.mp
-- 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₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hV₁ : MDiffAt[s] (T% V₁) x
hs : UniqueMDiffWithinAt I s x
⊢ UniqueDiffWithinAt 𝕜 ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
exact uniqueMDiffWithinAt_iff_inter_range.1 hs

Premises used: uniqueMDiffWithinAt_iff_inter_range, Iff.mp
-- 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 V₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt (T% V) x
hV₁ : MDiffAt (T% V₁) x
simp : mlieBracketWithin I (V + V₁) W univ x = mlieBracketWithin I V W univ x + mlieBracketWithin I V₁ W univ x
⊢ mlieBracket I (V + V₁) W x = mlieBracket I V W x + mlieBracket I V₁ W x

Tactic:
simp only [← mlieBracketWithin_univ] at hV hV₁ ⊢

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
x : M
V W V₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt (T% V) x
hV₁ : MDiffAt (T% V₁) x
⊢ mlieBracketWithin I (V + V₁) W univ x = mlieBracketWithin I V W univ x + mlieBracketWithin I V₁ W univ x

Tactic:
mlieBracketWithin_add_left hV hV₁ (uniqueMDiffWithinAt_univ _)

Premises used: VectorField.mlieBracketWithin_add_left, uniqueMDiffWithinAt_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
x : M
V W V₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt (T% V) x
hV₁ : MDiffAt (T% V₁) x
⊢ mlieBracketWithin I (V + V₁) W univ x = mlieBracketWithin I V W univ x + mlieBracketWithin I V₁ W univ x

Tactic:
exact mlieBracketWithin_add_left hV hV₁ (uniqueMDiffWithinAt_univ _)

Premises used: VectorField.mlieBracketWithin_add_left, uniqueMDiffWithinAt_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 : Set M
x : M
V W W₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hW : MDiffAt[s] (T% W) x
hW₁ : MDiffAt[s] (T% W₁) x
hs : UniqueMDiffWithinAt I s x
rw :
  -(mlieBracketWithin I W V s x + mlieBracketWithin I W₁ V s x) =
    -mlieBracketWithin I W V s x + -mlieBracketWithin I W₁ V s x
⊢ mlieBracketWithin I V (W + W₁) s x = mlieBracketWithin I V W s x + mlieBracketWithin I V W₁ s x

Tactic:
rw [mlieBracketWithin_swap, Pi.neg_apply, mlieBracketWithin_add_left hW hW₁ hs,
    mlieBracketWithin_swap (V := V), mlieBracketWithin_swap (V := V), Pi.neg_apply, Pi.neg_apply]

Premises used: VectorField.mlieBracketWithin_add_left, Pi.neg_apply, 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
x : M
V W W₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hW : MDiffAt[s] (T% W) x
hW₁ : MDiffAt[s] (T% W₁) x
hs : UniqueMDiffWithinAt I s x
⊢ -(mlieBracketWithin I W V s x + mlieBracketWithin I W₁ V s x) =
    -mlieBracketWithin I W V s x + -mlieBracketWithin I W₁ V s x

Tactic:
abel
-- 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 W₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hW : MDiffAt (T% W) x
hW₁ : MDiffAt (T% W₁) x
simp : mlieBracketWithin I V (W + W₁) univ x = mlieBracketWithin I V W univ x + mlieBracketWithin I V W₁ univ x
⊢ mlieBracket I V (W + W₁) x = mlieBracket I V W x + mlieBracket I V W₁ x

Tactic:
simp only [← mlieBracketWithin_univ] at hW hW₁ ⊢

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
x : M
V W W₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hW : MDiffAt (T% W) x
hW₁ : MDiffAt (T% W₁) x
⊢ mlieBracketWithin I V (W + W₁) univ x = mlieBracketWithin I V W univ x + mlieBracketWithin I V W₁ univ x

Tactic:
mlieBracketWithin_add_right hW hW₁ (uniqueMDiffWithinAt_univ _)

Premises used: uniqueMDiffWithinAt_univ, VectorField.mlieBracketWithin_add_right
-- 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 W₁ : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hW : MDiffAt (T% W) x
hW₁ : MDiffAt (T% W₁) x
⊢ mlieBracketWithin I V (W + W₁) univ x = mlieBracketWithin I V W univ x + mlieBracketWithin I V W₁ univ x

Tactic:
exact mlieBracketWithin_add_right hW hW₁ (uniqueMDiffWithinAt_univ _)

Premises used: uniqueMDiffWithinAt_univ, VectorField.mlieBracketWithin_add_right
-- 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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffWithinAt I s x
hV : MDiffAt[t] (T% V) x
hW : MDiffAt[t] (T% W) x
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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffWithinAt I s x
hV : MDiffAt[t] (T% V) x
hW : MDiffAt[t] (T% W) x
h :
  (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E) ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
h₁ : UniqueDiffWithinAt 𝕜 ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
h₂ :
  DifferentiableWithinAt 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
h₃ :
  DifferentiableWithinAt 𝕜 (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)
⊢ 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:
rw [lieBracketWithin_of_mem_nhdsWithin]

Premises used: VectorField.lieBracketWithin_of_mem_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 : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffWithinAt I s x
hV : MDiffAt[t] (T% V) x
hW : MDiffAt[t] (T% W) x
h :
  (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
h₁ : range (↑I : H → E) ∈ 𝓝[(↑(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) ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
apply Filter.inter_mem

Premises used: Filter.inter_mem