rw [((openEmbedding_coe.prod openEmbedding_coe).map_nhds_eq (m, n)).symm]
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n✝ : ℕ∞
m n : ℕ
⊢ 𝓝 (↑m, ↑n) = 𝓟 {(↑m, ↑n)}
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n✝ : ℕ∞
m n : ℕ
⊢ Filter.map (fun x => (↑x.1, ↑x.2)) (𝓝 (m, n)) = 𝓟 {(↑m, ↑n)}