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

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

State before:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t
⊢ a ∈ s
Tactic:
have ⟨u, hu₁, hu₂, hu₃⟩ := hs
State after:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t
u : Set α
hu₁ : u ⊆ s
hu₂ : sets τ u
hu₃ : a ∈ u
⊢ a ∈ s

State before:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t
u : Set α
hu₁ : u ⊆ s
hu₂ : sets τ u
hu₃ : a ∈ u
⊢ a ∈ s
Tactic:
exact hu₁ hu₃
State after:
no goals