-- Mathlib/Geometry/Manifold/VectorField.lean
theorem _root_.Filter.EventuallyEq.mlieBracketWithin_vectorField_eq
    (hV : V₁ =ᶠ[𝓝[s] x] V) (hxV : V₁ x = V x) (hW : W₁ =ᶠ[𝓝[s] x] W) (hxW : W₁ x = W x) :
    mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x

Proof state:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : 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) x)) := inferInstanceAs (NormedAddCommGroup E)
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inferInstanceAs (NormedSpace 𝕜 E)
y : TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)
hy : y ∈ ↑(extChartAt I x).symm ⁻¹' {x | V₁ x = V x}
⊢ mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V₁ (range ↑I) y =
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) y

Tactic:
simp only [mpullbackWithin_apply]

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : 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) x)) := inferInstanceAs (NormedAddCommGroup E)
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inferInstanceAs (NormedSpace 𝕜 E)
y : TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)
hy : y ∈ ↑(extChartAt I x).symm ⁻¹' {x | V₁ x = V x}
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) y).inverse (V₁ (↑(extChartAt I x).symm y)) =
    (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) y).inverse (V (↑(extChartAt I x).symm y))

Proof state:
case h.e_6.h.hxW
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : 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) x)) := inferInstanceAs (NormedAddCommGroup E)
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inferInstanceAs (NormedSpace 𝕜 E)
⊢ mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W₁ (range ↑I) (↑(extChartAt I x) x) =
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I) (↑(extChartAt I x) x)

Tactic:
simp only [mpullbackWithin_apply]

Result:
case h.e_6.h.hxW
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : 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) x)) := inferInstanceAs (NormedAddCommGroup E)
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inferInstanceAs (NormedSpace 𝕜 E)
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)).inverse
      (W₁ (↑(extChartAt I x).symm (↑(extChartAt I x) x))) =
    (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)).inverse
      (W (↑(extChartAt I x).symm (↑(extChartAt I x) x)))

Proof state:
case h.e_6.h.hW
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : 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) x)) := inferInstanceAs (NormedAddCommGroup E)
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inferInstanceAs (NormedSpace 𝕜 E)
⊢ mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W₁
      (range ↑I) =ᶠ[𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x]
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)

Tactic:
apply nhdsWithin_mono _ inter_subset_left

Result:
case h.e_6.h.hW.a
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : 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) x)) := inferInstanceAs (NormedAddCommGroup E)
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inferInstanceAs (NormedSpace 𝕜 E)
⊢ {x_1 |
      (fun x_2 =>
          mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W₁ (range ↑I) x_2 =
            mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I) x_2)
        x_1} ∈
    𝓝[↑(extChartAt I x).symm ⁻¹' s] ↑(extChartAt I x) x

Proof state:
case h.e_6.h.hxW.h.e_6.h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : 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) x)) := inferInstanceAs (NormedAddCommGroup E)
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inferInstanceAs (NormedSpace 𝕜 E)
⊢ W₁ (↑(extChartAt I x).symm (↑(extChartAt I x) x)) = W (↑(extChartAt I x).symm (↑(extChartAt I x) x))

Tactic:
convert hxW <;> exact extChartAt_to_inv x

Result:
no goals