Theorem: ENat.nhds_cast_cast (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n✝ : ℕ∞
m n : ℕ
⊢ 𝓝 (↑m, ↑n) = 𝓟 {(↑m, ↑n)}
Tactic:
rw [((openEmbedding_coe.prod openEmbedding_coe).map_nhds_eq (m, n)).symm]
State after:
α : 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)}

State before:
α : 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)}
Tactic:
simp
State after:
no goals