rw [nhds_cast_eq, principal_singleton, eventually_pure, Nat.cast_pos,
  ← Nat.ne_zero_iff_zero_lt]
case inr.intro
x b : ℕ
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ⊤ ≠ ⊤
h : ↑b ≤ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 ↑b, 0 < y
case inr.intro
x b : ℕ
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ⊤ ≠ ⊤
h : ↑b ≤ ⊤
⊢ b ≠ 0