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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ (↑(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)

Tactic:
preimage_extChartAt_eventuallyEq_compl_singleton y h

Premises used: preimage_extChartAt_eventuallyEq_compl_singleton
-- 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
⊢ (↑(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)

Tactic:
exact preimage_extChartAt_eventuallyEq_compl_singleton y h

Premises used: preimage_extChartAt_eventuallyEq_compl_singleton
-- 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
h : s =ᶠ[𝓝 x] t
⊢ mlieBracketWithin I V W s x = mlieBracketWithin I V W t x

Tactic:
mlieBracketWithin_congr_set' x <| h.filter_mono inf_le_left

Premises used: Filter.EventuallyEq.filter_mono, VectorField.mlieBracketWithin_congr_set', inf_le_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 t : Set M
x : M
V W : (x : M) → TangentSpace I x
ht : t ∈ 𝓝 x
h : s ∩ t =ᶠ[𝓝 x] s
⊢ mlieBracketWithin I V W (s ∩ t) x = mlieBracketWithin I V W s x

Tactic:
apply mlieBracketWithin_congr_set

Premises used: VectorField.mlieBracketWithin_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
ht : t ∈ 𝓝 x
h : ∀ (y : M) (hy : y ∈ t), (s ∩ t) y = s y
⊢ s ∩ t =ᶠ[𝓝 x] s

Tactic:
filter_upwards [ht] with y hy
-- 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
ht : t ∈ 𝓝 x
y : M
hy : y ∈ t
h : (y ∈ s ∩ t) = (y ∈ s)
⊢ (s ∩ t) y = s y

Tactic:
change (y ∈ s ∩ t) = (y ∈ s)

Premises used: Membership.mem, Inter.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
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
ht : t ∈ 𝓝 x
y : M
hy : y ∈ t
⊢ (y ∈ s ∩ t) = (y ∈ s)

Tactic:
simp_all
-- 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
h : s ∈ 𝓝 x
rw : mlieBracketWithin I V W s x = mlieBracketWithin I V W univ x
rw₁ : mlieBracketWithin I V W (univ ∩ s) x = mlieBracketWithin I V W univ x
rw₂ rw₃ : mlieBracketWithin I V W univ x = mlieBracketWithin I V W univ x
⊢ mlieBracketWithin I V W s x = mlieBracket I V W x

Tactic:
rw [← mlieBracketWithin_univ, ← univ_inter s, mlieBracketWithin_inter h]

Premises used: VectorField.mlieBracketWithin_inter, Set.univ_inter, 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
hs : IsOpen[inst_4] s
hx : x ∈ s
⊢ mlieBracketWithin I V W s x = mlieBracket I V W x

Tactic:
mlieBracketWithin_of_mem_nhds (hs.mem_nhds hx)

Premises used: VectorField.mlieBracketWithin_of_mem_nhds, IsOpen.mem_nhds
-- 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
⊢ mlieBracketWithin I V W s =ᶠ[𝓝 x] mlieBracketWithin I V W t

Tactic:
(eventually_nhds_nhdsWithin.2 h).mono fun _ => mlieBracketWithin_congr_set' y

Premises used: Iff.mpr, eventually_nhds_nhdsWithin, VectorField.mlieBracketWithin_congr_set', Filter.EventuallyEq, Filter.Eventually.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
h : s =ᶠ[𝓝 x] t
⊢ mlieBracketWithin I V W s =ᶠ[𝓝 x] mlieBracketWithin I V W t

Tactic:
mlieBracketWithin_eventually_congr_set' x <| h.filter_mono inf_le_left

Premises used: Filter.EventuallyEq.filter_mono, VectorField.mlieBracketWithin_eventually_congr_set', inf_le_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₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
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) ⁻¹' s ∩ 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) ⁻¹' s ∩ 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 : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
h :
  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]
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))
h₁ :
  Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
h₂ :
  mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁
      (range
        (↑I : H → E)) =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (range (↑I : H → E))
h₃ :
  Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W₁ (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) W (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) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
apply Filter.EventuallyEq.lieBracketWithin_vectorField_eq

Premises used: Filter.EventuallyEq.lieBracketWithin_vectorField_eq
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
h :
  {x_1 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) |
      (fun (x_2 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) ↦
          Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)) x_2 :
              TangentSpace 𝓘(𝕜, E) x_2)
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2))
        x_1} ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x
⊢ mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁
      (range
        (↑I : H → E)) =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E))

Tactic:
apply nhdsWithin_mono _ inter_subset_left

Premises used: Set.inter_subset_left, nhdsWithin_mono
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
⊢ x =
    (↑(extChartAt I x).symm : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) → M)
      ((↑(extChartAt I x) : M → TangentSpace 𝓘(𝕜, E) ((↑(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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
h :
  ∀ (y : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    (hy :
      y ∈ (↑(extChartAt I x).symm : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) → M) ⁻¹' {x : M | V₁ x = V x}),
    Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)) y : TangentSpace 𝓘(𝕜, E) y)
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) y)
⊢ {x_1 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) |
      (fun (x_2 : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) ↦
          Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V₁ (range (↑I : H → E)) x_2 :
              TangentSpace 𝓘(𝕜, E) x_2)
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) V (range (↑I : H → E)) x_2))
        x_1} ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s] (↑(extChartAt I x) : M → E) x

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

Premises used: ContinuousAt.continuousWithinAt, ContinuousWithinAt.preimage_mem_nhdsWithin'', continuousAt_extChartAt_symm
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
y : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)
hy : y ∈ (↑(extChartAt I x).symm : TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x) → M) ⁻¹' {x : M | V₁ x = V x}
⊢ Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    ((ContinuousLinearMap.inverse (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) :
        (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) y)) → TangentSpace 𝓘(𝕜, E) y)
      (V₁ ((↑(extChartAt I x).symm : E → M) y)))
    ((ContinuousLinearMap.inverse (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) :
        (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) y)) → TangentSpace 𝓘(𝕜, E) y)
      (V ((↑(extChartAt I x).symm : E → M) y)))

Tactic:
congr 1
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
h :
  Eq.{u_3 + 1} (α := TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (V₁ ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (V ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
⊢ Eq (α := TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
    ((ContinuousLinearMap.inverse
          (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
            ((↑(extChartAt I x) : M → E) x)) :
        (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) →
          TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
      (V₁ ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))))
    ((ContinuousLinearMap.inverse
          (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
            ((↑(extChartAt I x) : M → E) x)) :
        (a : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) →
          TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x))
      (V ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))))

Tactic:
congr 1
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
⊢ V₁ x = V x

Tactic:
hxV
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
h : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x
h₁ h₂ :
  TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)) = TangentSpace I x →
    (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x
⊢ Eq.{u_3 + 1} (α := TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (V₁ ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))
    (V ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)))

Tactic:
convert! hxV
-- Module: Mathlib.Geometry.Manifold.VectorField.LieBracket
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_7, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
_I2 : NormedSpace.{u_1, u_3} 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) x)) := inst_3
⊢ (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x

Tactic:
extChartAt_to_inv x

Premises used: extChartAt_to_inv