Theorem: FilterGame.TopologicalSpace.nhds_le_of_le (FilterGame/Solutions/Topology.lean)

State before:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
hsf : 𝓟 s ≤ f
⊢ 𝓝 a ≤ f
Tactic:
intros u hu
State after:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
hsf : 𝓟 s ≤ f
u : Set α
hu : u ∈ f
⊢ u ∈ 𝓝 a

State before:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
hsf : 𝓟 s ≤ f
u : Set α
hu : u ∈ f
⊢ u ∈ 𝓝 a
Tactic:
rw [mem_nhds_def]
State after:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
hsf : 𝓟 s ≤ f
u : Set α
hu : u ∈ f
⊢ ∃ t, t ⊆ u ∧ sets τ t ∧ a ∈ t

State before:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
hsf : 𝓟 s ≤ f
u : Set α
hu : u ∈ f
⊢ ∃ t, t ⊆ u ∧ sets τ t ∧ a ∈ t
Tactic:
specialize hsf _ hu
State after:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
u : Set α
hu : u ∈ f
hsf : u ∈ 𝓟 s
⊢ ∃ t, t ⊆ u ∧ sets τ t ∧ a ∈ t

State before:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
u : Set α
hu : u ∈ f
hsf : u ∈ 𝓟 s
⊢ ∃ t, t ⊆ u ∧ sets τ t ∧ a ∈ t
Tactic:
rw [Filter.mem_principal_def] at hsf
State after:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
u : Set α
hu : u ∈ f
hsf : s ⊆ u
⊢ ∃ t, t ⊆ u ∧ sets τ t ∧ a ∈ t

State before:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
u : Set α
hu : u ∈ f
hsf : s ⊆ u
⊢ ∃ t, t ⊆ u ∧ sets τ t ∧ a ∈ t
Tactic:
exact ⟨s, hsf, ho, h⟩
State after:
no goals