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

State before:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ s ∈ 𝓝 a ↔ a ∈ s
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ s ∈ 𝓝 a → a ∈ s

case mpr
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ a ∈ s → s ∈ 𝓝 a

State before:
case mp
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ s ∈ 𝓝 a → a ∈ s

case mpr
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ a ∈ s → s ∈ 𝓝 a
Tactic:
. exact mem_of_mem_nhds
State after:
case mpr
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ a ∈ s → s ∈ 𝓝 a

State before:
case mpr
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ a ∈ s → s ∈ 𝓝 a
Tactic:
. exact mem_nhds hs
State after:
no goals

State before:
case mp
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ s ∈ 𝓝 a → a ∈ s
Tactic:
exact mem_of_mem_nhds
State after:
no goals

State before:
case mpr
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ a ∈ s → s ∈ 𝓝 a
Tactic:
exact mem_nhds hs
State after:
no goals