rw [← Nat.cast_mul, nhds_cast_cast, nhds_cast_eq]
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))
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)})