rw [top_mul (by simpa using hb), tendsto_nhds_top_iff]
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 (⊤ * b))
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
⊢ ∀ (x : ℕ), ∀ᶠ (a : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < a.1 * a.2