no goals
α✝ : Type ?u.81510
β : Type ?u.81513
γ : Type ?u.81516
δ : Type ?u.81519
inst✝² : TopologicalSpace α✝
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Finite ι
inst✝ : (i : ι) → TopologicalSpace (α i)
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ 𝓝[Set.pi univ s] x = ⨅ (i : ι), comap (fun x => x i) (𝓝[s i] x i)
simpa [nhdsWithin] using nhdsWithin_pi_eq finite_univ s x