obtain (rfl | ha') := eq_or_ne a ⊤
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : b ≤ a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 (⊤ * b))

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))