Theorem: ENat.mem_nhds_iff (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n x : ℕ∞
s : Set ℕ∞
hx : x ≠ ⊤
⊢ s ∈ 𝓝 x ↔ x ∈ s
Tactic:
rw [_root_.mem_nhds_iff]
State after:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n x : ℕ∞
s : Set ℕ∞
hx : x ≠ ⊤
⊢ (∃ t ⊆ s, IsOpen t ∧ x ∈ t) ↔ x ∈ s

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n x : ℕ∞
s : Set ℕ∞
hx : x ≠ ⊤
⊢ (∃ t ⊆ s, IsOpen t ∧ x ∈ t) ↔ x ∈ s
Tactic:
exact ⟨fun ⟨_, h, _, h'⟩ ↦ h h', fun h ↦ ⟨_, singleton_subset_iff.2 h, isOpen_singleton hx, rfl⟩⟩
State after:
no goals