no goals
α : Type u_1
β : Type ?u.12030
γ : Type ?u.12033
δ : Type ?u.12036
inst✝ : TopologicalSpace α
a : α
s t u : Set α
hs : s ∈ 𝓝 a
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t] a = 𝓝[u] a
rw [nhdsWithin_restrict' t hs, nhdsWithin_restrict' u hs, h₂]