no goals
α : Type u_1
β : Type ?u.304019
γ : Type ?u.304022
δ : Type ?u.304025
inst✝ : TopologicalSpace α
s : Set α
a : ↑s
t : Set ↑s
⊢ t ∈ 𝓝 a ↔ Subtype.val '' t ∈ 𝓝[s] ↑a
rw [← map_nhds_subtype_val, image_mem_map_iff Subtype.val_injective]