obtain (rfl | hbne) := eq_or_ne b ⊤
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 b, 0 < y
case inl
x : ℕ
ha hb : ⊤ ≠ 0 ∨ ⊤ ≠ ⊤
h : ⊤ ≤ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 ⊤, 0 < y

case inr
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hbne : b ≠ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 b, 0 < y