no goals
α✝ : Type ?u.23519
β : Type ?u.23522
γ : Type ?u.23525
δ : Type ?u.23528
inst✝¹ : TopologicalSpace α✝
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (α i)
I : Set ι
hI : Set.Finite I
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ 𝓝[Set.pi I s] x = ⨅ (i : ι), comap (fun x => x i) (𝓝 (x i) ⊓ ⨅ (_ : i ∈ I), 𝓟 (s i))
simp only [nhdsWithin, nhds_pi, Filter.pi, comap_inf, comap_iInf, pi_def, comap_principal, ←
  iInf_principal_finite hI, ← iInf_inf_eq]