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
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₀
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)) →L[𝕜]
      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₀)))
    (mfderiv% (↑(extChartAt I x₀) : M → E) x₀)
V' : (x : E') → TangentSpace 𝓘(𝕜, E') x :=
  mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') V (range (↑I' : H' → E'))
hV' : V' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') V (range (↑I' : H' → E'))
W' : (x : E') → TangentSpace 𝓘(𝕜, E') x :=
  mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') W (range (↑I' : H' → E'))
hW' : W' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') W (range (↑I' : H' → E'))
F : E → E' := ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f) ∘ (↑(extChartAt I x₀).symm : E → M)
hF : F = ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f) ∘ (↑(extChartAt I x₀).symm : E → M)
hFx₀ : (↑(extChartAt I' (f x₀)) : M' → E') (f x₀) = F ((↑(extChartAt I x₀) : M → E) x₀)
P :
  ∀ (Y : (x : M') → TangentSpace I' x),
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (mpullbackWithin I I' f Y s)
        (range
          (↑I :
            H → E)) =ᶠ[𝓝[(↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x₀) : M → E) x₀]
      mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') F
        (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') Y (range (↑I' : H' → E')))
        ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
hu₁ : UniqueDiffOn 𝕜 ((extChartAt I x₀).target ∩ (↑(extChartAt I x₀).symm : E → M) ⁻¹' s)
⊢ UniqueDiffOn 𝕜 ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target)

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- 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₀
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)) →L[𝕜]
      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₀)))
    (mfderiv% (↑(extChartAt I x₀) : M → E) x₀)
V' : (x : E') → TangentSpace 𝓘(𝕜, E') x :=
  mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') V (range (↑I' : H' → E'))
hV' : V' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') V (range (↑I' : H' → E'))
W' : (x : E') → TangentSpace 𝓘(𝕜, E') x :=
  mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') W (range (↑I' : H' → E'))
hW' : W' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') W (range (↑I' : H' → E'))
F : E → E' := ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f) ∘ (↑(extChartAt I x₀).symm : E → M)
hF : F = ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f) ∘ (↑(extChartAt I x₀).symm : E → M)
hFx₀ : (↑(extChartAt I' (f x₀)) : M' → E') (f x₀) = F ((↑(extChartAt I x₀) : M → E) x₀)
P :
  ∀ (Y : (x : M') → TangentSpace I' x),
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (mpullbackWithin I I' f Y s)
        (range
          (↑I :
            H → E)) =ᶠ[𝓝[(↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x₀) : M → E) x₀]
      mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') F
        (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') Y (range (↑I' : H' → E')))
        ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
⊢ UniqueDiffOn 𝕜 ((extChartAt I x₀).target ∩ (↑(extChartAt I x₀).symm : E → M) ⁻¹' s)

Tactic:
UniqueMDiffOn.uniqueDiffOn_target_inter hu x₀

Premises used: UniqueMDiffOn.uniqueDiffOn_target_inter
-- 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₀
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)) →L[𝕜]
      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₀)))
    (mfderiv% (↑(extChartAt I x₀) : M → E) x₀)
V' : (x : E') → TangentSpace 𝓘(𝕜, E') x :=
  mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') V (range (↑I' : H' → E'))
hV' : V' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') V (range (↑I' : H' → E'))
W' : (x : E') → TangentSpace 𝓘(𝕜, E') x :=
  mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') W (range (↑I' : H' → E'))
hW' : W' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') W (range (↑I' : H' → E'))
F : E → E' := ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f) ∘ (↑(extChartAt I x₀).symm : E → M)
hF : F = ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f) ∘ (↑(extChartAt I x₀).symm : E → M)
hFx₀ : (↑(extChartAt I' (f x₀)) : M' → E') (f x₀) = F ((↑(extChartAt I x₀) : M → E) x₀)
P :
  ∀ (Y : (x : M') → TangentSpace I' x),
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (mpullbackWithin I I' f Y s)
        (range
          (↑I :
            H → E)) =ᶠ[𝓝[(↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x₀) : M → E) x₀]
      mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') F
        (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') Y (range (↑I' : H' → E')))
        ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
⊢ UniqueDiffOn 𝕜 ((extChartAt I x₀).target ∩ (↑(extChartAt I x₀).symm : E → M) ⁻¹' s)

Tactic:
exact UniqueMDiffOn.uniqueDiffOn_target_inter hu x₀

Premises used: UniqueMDiffOn.uniqueDiffOn_target_inter
-- 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₀
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)) →L[𝕜]
      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₀)))
    (mfderiv% (↑(extChartAt I x₀) : M → E) x₀)
V' : (x : E') → TangentSpace 𝓘(𝕜, E') x :=
  mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') V (range (↑I' : H' → E'))
hV' : V' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') V (range (↑I' : H' → E'))
W' : (x : E') → TangentSpace 𝓘(𝕜, E') x :=
  mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') W (range (↑I' : H' → E'))
hW' : W' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') W (range (↑I' : H' → E'))
F : E → E' := ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f) ∘ (↑(extChartAt I x₀).symm : E → M)
hF : F = ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f) ∘ (↑(extChartAt I x₀).symm : E → M)
hFx₀ : (↑(extChartAt I' (f x₀)) : M' → E') (f x₀) = F ((↑(extChartAt I x₀) : M → E) x₀)
P :
  ∀ (Y : (x : M') → TangentSpace I' x),
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (mpullbackWithin I I' f Y s)
        (range
          (↑I :
            H → E)) =ᶠ[𝓝[(↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x₀) : M → E) x₀]
      mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') F
        (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') Y (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) ⁻¹' s ∩ (extChartAt I x₀).target

Tactic:
simp [hx₀]
-- 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₀
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)) →L[𝕜]
      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₀)))
    (mfderiv% (↑(extChartAt I x₀) : M → E) x₀)
V' : (x : E') → TangentSpace 𝓘(𝕜, E') x :=
  mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') V (range (↑I' : H' → E'))
hV' : V' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') V (range (↑I' : H' → E'))
W' : (x : E') → TangentSpace 𝓘(𝕜, E') x :=
  mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') W (range (↑I' : H' → E'))
hW' : W' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') W (range (↑I' : H' → E'))
F : E → E' := ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f) ∘ (↑(extChartAt I x₀).symm : E → M)
hF : F = ((↑(extChartAt I' (f x₀)) : M' → E') ∘ f) ∘ (↑(extChartAt I x₀).symm : E → M)
hFx₀ : (↑(extChartAt I' (f x₀)) : M' → E') (f x₀) = F ((↑(extChartAt I x₀) : M → E) x₀)
P :
  ∀ (Y : (x : M') → TangentSpace I' x),
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm : E → M) (mpullbackWithin I I' f Y s)
        (range
          (↑I :
            H → E)) =ᶠ[𝓝[(↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x₀) : M → E) x₀]
      mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') F
        (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm : E' → M') Y (range (↑I' : H' → E')))
        ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
z : E
hz : z ∈ (↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target
⊢ f ((↑(extChartAt I x₀).symm : E → M) z) ∈ t

Tactic:
hst hz.1

Premises used: And.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
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
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 : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
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
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 : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
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
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 : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
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₀
pos :
  ∀
    (hfi :
      ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀))
        (mfderivWithin I I' f s 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₀)
neg :
  ∀
    (hfi :
      ¬ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀))
          (mfderivWithin I I' f s 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₀)
⊢ 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:
by_cases hfi : (mfderiv[s] f x₀).IsInvertible

Premises used: ContinuousLinearMap.IsInvertible, mfderivWithin
-- 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
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 : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
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₀
hfi :
  ¬ContinuousLinearMap.IsInvertible (M := TangentSpace I x₀) (M₂ := TangentSpace I' (f x₀)) (mfderivWithin I I' f s x₀)
neg :
  Eq (α := TangentSpace I x₀) (0 : 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,
      ContinuousLinearMap.inverse_of_not_isInvertible hfi, ContinuousLinearMap.zero_apply]

Premises used: ContinuousLinearMap.inverse_of_not_isInvertible, VectorField.mpullbackWithin_apply, VectorField.mlieBracketWithin_apply, ContinuousLinearMap.zero_apply