rw [nhds_swap a b, mul_comm, tendsto_map'_iff]
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : ¬b ≤ a
h' : Tendsto (fun p => p.1 * p.2) (𝓝 (b, a)) (𝓝 (b * a))
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : ¬b ≤ a
h' : Tendsto (fun p => p.1 * p.2) (𝓝 (b, a)) (𝓝 (b * a))
⊢ Tendsto ((fun p => p.1 * p.2) ∘ Prod.swap) (𝓝 (b, a)) (𝓝 (b * a))