-- Mathlib/Geometry/Manifold/VectorField.lean
theorem _root_.Filter.EventuallyEq.mlieBracketWithin_vectorField'
    (hV : V₁ =ᶠ[𝓝[s] x] V) (hW : W₁ =ᶠ[𝓝[s] x] W) (ht : t ⊆ s) :
    mlieBracketWithin I V₁ W₁ t =ᶠ[𝓝[s] x] mlieBracketWithin I V W t

Proof state:
case h.hV.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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ {x | (fun x => V₁ x = V x) x} ∈ 𝓝[s] y

Tactic:
exact hVy'

Result:
no goals

Proof state:
case 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ W₁ =ᶠ[𝓝[t] y] W

Tactic:
apply nhdsWithin_mono _ ht

Result:
case 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ {x | (fun x => W₁ x = W x) x} ∈ 𝓝[s] y

Proof state:
𝕜 : 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
⊢ mlieBracketWithin I V₁ W₁ t =ᶠ[𝓝[s] x] mlieBracketWithin I V W t

Tactic:
filter_upwards [hV, hW, eventually_eventually_nhdsWithin.2 hV,
  eventually_eventually_nhdsWithin.2 hW] with y hVy hWy hVy' hWy'

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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ mlieBracketWithin I V₁ W₁ t y = mlieBracketWithin I V W t y

Proof state:
case 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ W₁ y = W y

Tactic:
exact hWy

Result:
no goals

Proof state:
case h.hxV
𝕜 : 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ V₁ y = V y

Tactic:
exact hVy

Result:
no goals

Proof state:
case 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ {x | (fun x => W₁ x = W x) x} ∈ 𝓝[s] y

Tactic:
exact hWy'

Result:
no goals

Proof state:
case h.hV
𝕜 : 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ V₁ =ᶠ[𝓝[t] y] V

Tactic:
apply nhdsWithin_mono _ ht

Result:
case h.hV.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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ {x | (fun x => V₁ x = V x) x} ∈ 𝓝[s] y