lift b to ℕ using (h.trans_lt (WithTop.coe_lt_top a)).ne
case inr.intro
b : ℕ∞
a : ℕ
ha : ↑a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ↑a ≠ ⊤
h : b ≤ ↑a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, b)) (𝓝 (↑a * b))
case inr.intro.intro
a b : ℕ
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ↑a ≠ ⊤
h : ↑b ≤ ↑a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, ↑b)) (𝓝 (↑a * ↑b))