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 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
⊢ x = (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) 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 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
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
apply nhdsWithin_mono _ inter_subset_left <|
        (continuousAt_extChartAt_symm x).continuousWithinAt.preimage_mem_nhdsWithin'' st (by simp)

Premises used: ContinuousAt.continuousWithinAt, ContinuousWithinAt.preimage_mem_nhdsWithin'', Set.inter_subset_left, continuousAt_extChartAt_symm, 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 : (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
⊢ range (↑I : H → E) ∈ 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
nhdsWithin_mono _ inter_subset_right self_mem_nhdsWithin

Premises used: self_mem_nhdsWithin, nhdsWithin_mono, Set.inter_subset_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
⊢ range (↑I : H → E) ∈ 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
exact nhdsWithin_mono _ inter_subset_right self_mem_nhdsWithin

Premises used: self_mem_nhdsWithin, nhdsWithin_mono, Set.inter_subset_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
⊢ 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 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
⊢ 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
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
⊢ 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)

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 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
⊢ 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)

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 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
⊢ 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)

Tactic:
hW.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 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
⊢ 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)

Tactic:
exact hW.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 t : Set M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
st : s ⊆ t
ht : UniqueMDiffWithinAt I s x
hV : MDiffAt[t] (T% V) x
hW : MDiffAt[t] (T% W) x
⊢ mlieBracketWithin I V W s x = mlieBracketWithin I V W t x

Tactic:
mlieBracketWithin_of_mem_nhdsWithin (nhdsWithin_mono _ st self_mem_nhdsWithin) ht hV hW

Premises used: VectorField.mlieBracketWithin_of_mem_nhdsWithin, self_mem_nhdsWithin, 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 : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hs : UniqueMDiffWithinAt I s x
hV : MDiffAt (T% V) x
hW : MDiffAt (T% W) x
⊢ MDiffAt[univ] (T% V) x

Tactic:
simp only [← mlieBracketWithin_univ, ← mdifferentiableWithinAt_univ] at hV hW ⊢

Premises used: mdifferentiableWithinAt_univ, 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 : Set M
x : M
V W : (x : M) → TangentSpace I x
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hs : UniqueMDiffWithinAt I s x
hV : MDiffAt (T% V) x
hW : MDiffAt (T% W) x
hV₁ : MDiffAt[univ] (T% V) x
⊢ MDiffAt[univ] (T% W) x

Tactic:
simp only [← mlieBracketWithin_univ, ← mdifferentiableWithinAt_univ] at hV hW ⊢

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

Tactic:
mlieBracketWithin_subset (subset_univ _) hs hV hW

Premises used: Set.subset_univ, VectorField.mlieBracketWithin_subset
-- 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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hs : UniqueMDiffWithinAt I s x
hV : MDiffAt[univ] (T% V) x
hW : MDiffAt[univ] (T% W) x
⊢ mlieBracketWithin I V W s x = mlieBracketWithin I V W univ x

Tactic:
exact mlieBracketWithin_subset (subset_univ _) hs hV hW

Premises used: Set.subset_univ, VectorField.mlieBracketWithin_subset
-- 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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hVs : EqOn V₁ V t
hVx : V₁ x = V x
hW : MDiffAt[s] (T% W) x
hWs : EqOn W₁ W t
hWx : W₁ x = W x
hxt : UniqueMDiffWithinAt I t x
h₁ : t ⊆ s
rw : mlieBracketWithin I V W t x = mlieBracketWithin I V W s x
⊢ mlieBracketWithin I V₁ W₁ t x = mlieBracketWithin I V W s x

Tactic:
rw [mlieBracketWithin_congr hVs hVx hWs hWx]

Premises used: VectorField.mlieBracketWithin_congr
-- 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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hVs : EqOn V₁ V t
hVx : V₁ x = V x
hW : MDiffAt[s] (T% W) x
hWs : EqOn W₁ W t
hWx : W₁ x = W x
hxt : UniqueMDiffWithinAt I t x
h₁ : t ⊆ s
⊢ mlieBracketWithin I V W t x = mlieBracketWithin I V W s x

Tactic:
mlieBracketWithin_subset h₁ hxt hV hW

Premises used: VectorField.mlieBracketWithin_subset
-- 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
inst_6 : IsManifold I 2 M
inst_7 : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hVs : EqOn V₁ V t
hVx : V₁ x = V x
hW : MDiffAt[s] (T% W) x
hWs : EqOn W₁ W t
hWx : W₁ x = W x
hxt : UniqueMDiffWithinAt I t x
h₁ : t ⊆ s
⊢ mlieBracketWithin I V W t x = mlieBracketWithin I V W s x

Tactic:
exact mlieBracketWithin_subset h₁ hxt hV hW

Premises used: VectorField.mlieBracketWithin_subset
-- 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
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
inst_14 : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
⊢ (↑(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
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
inst_14 : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
⊢ (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀

Tactic:
have A : (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
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
inst_14 : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
⊢ x₀ = (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) 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
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
inst_14 : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
⊢ x₀ = (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)

Tactic:
have A' : x₀ = (extChartAt I x₀).symm (extChartAt I 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
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
inst_14 : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
A' : x₀ = (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)
⊢ MDiffAt[s] f x₀

Tactic:
have h'f : MDiffAt[s] f x₀ := (hf x₀ hx₀).mdifferentiableWithinAt two_ne_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
H' : Type u_5
inst_6 : TopologicalSpace H'
E' : Type u_6
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 2 M
inst_12 : IsManifold I' 2 M'
inst_13 : CompleteSpace E
inst_14 : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiffOn I s
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f ∘ (↑(extChartAt I x₀).symm : E → M))
    ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
A : (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀) = x₀
A' : x₀ = (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)
h'f : MDiffAt[s] f x₀
simp :
  Eq.{u_3 + 1} (α := TangentSpace I x₀)
    (((ContinuousLinearMap.inverse (mfderivWithin I I' f s x₀) :
            ContinuousLinearMap.{u_1, u_1, u_6, u_3} (RingHom.id 𝕜) (TangentSpace I' (f x₀)) (TangentSpace I x₀)) :
          (a : TangentSpace I' (f x₀)) → TangentSpace I x₀)
        ((ContinuousLinearMap.inverse (mfderiv% (↑(extChartAt I' (f x₀)) : M' → E') (f x₀)) :
            (a : TangentSpace 𝓘(𝕜, E') ((↑(extChartAt I' (f x₀)) : M' → E') (f x₀))) → TangentSpace I' (f x₀))
          (lieBracketWithin 𝕜
            (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') V (range (↑I' : H' → E')))
            (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') W (range (↑I' : H' → E')))
            ((↑(extChartAt I' (f x₀)).symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E'))
            ((↑(extChartAt I' (f x₀)) : M' → E') (f 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) (mpullbackWithin I I' f V s)
            (range (↑I : H → E)))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (mpullbackWithin I I' f W s)
            (range (↑I : H → E)))
          ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)) :
      TangentSpace I x₀)
⊢ Eq (α := TangentSpace I x₀) (mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀)
    (mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀)

Tactic:
simp only [mlieBracketWithin_apply, mpullbackWithin_apply]

Premises used: VectorField.mpullbackWithin_apply, VectorField.mlieBracketWithin_apply