no goals
α : Type u_1
β : Type ?u.302592
γ : Type ?u.302595
δ : Type ?u.302598
inst✝ : TopologicalSpace α
s : Set α
a : { x // x ∈ s }
t u : Set { x // x ∈ s }
⊢ t ∈ 𝓝[u] a ↔ t ∈ comap Subtype.val (𝓝[Subtype.val '' u] ↑a)
rw [nhdsWithin, nhds_subtype, principal_subtype, ← comap_inf, ← nhdsWithin]