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

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
hn : n ≠ ⊤
⊢ 𝓝 n = 𝓟 {n}
Tactic:
lift n to ℕ using hn
State after:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ
⊢ 𝓝 ↑n = 𝓟 {↑n}

State before:
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ
⊢ 𝓝 ↑n = 𝓟 {↑n}
Tactic:
simp
State after:
no goals