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

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
m : ℕ
⊢ 𝓝 (↑m, ⊤) = 𝓟 {↑m} ×ˢ ⨅ a, ⨅ (_ : a ≠ ⊤), 𝓟 (Ioi a)
Tactic:
rw [nhds_prod_eq, nhds_cast_eq, nhds_top, principal_singleton]
State after:
no goals