lift a to ℕ using ha'
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : b ≤ a
ha' : a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
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))