no goals
α : Type u
β : Type v
γ : Type ?u.158814
δ : Type ?u.158817
ε : Type ?u.158820
ζ : Type ?u.158823
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
s : Set α
a : ↑s
⊢ map Subtype.val (𝓝 a) = 𝓝[s] ↑a
rw [inducing_subtype_val.map_nhds_eq, Subtype.range_val]