Theorem: ENat.nhds_top' (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
⊢ 𝓝 ⊤ = ⨅ a, 𝓟 (Ioi ↑a)
Tactic:
refine nhds_top.trans <| iInf_ne_top _
State after:
no goals