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

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n✝ : ℕ∞
n : ℕ
⊢ 𝓝 ↑n = 𝓟 {↑n}
Tactic:
ext
State after:
case a
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n✝ : ℕ∞
n : ℕ
s✝ : Set ℕ∞
⊢ s✝ ∈ 𝓝 ↑n ↔ s✝ ∈ 𝓟 {↑n}

State before:
case a
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n✝ : ℕ∞
n : ℕ
s✝ : Set ℕ∞
⊢ s✝ ∈ 𝓝 ↑n ↔ s✝ ∈ 𝓟 {↑n}
Tactic:
simp
State after:
no goals