Theorem: FilterGame.TopologicalSpace.OpenSets.mem_nhds (FilterGame/Solutions/Topology.lean)

State before:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
ha : a ∈ s
⊢ s ∈ 𝓝 a
Tactic:
rw [mem_nhds_def]
State after:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
ha : a ∈ s
⊢ ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t

State before:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
ha : a ∈ s
⊢ ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t
Tactic:
exact ⟨s, rfl.subset, hs, ha⟩
State after:
no goals