no goals
α✝ : Type ?u.191155
β : Type ?u.191158
γ : Type ?u.191161
δ : Type ?u.191164
inst✝¹ : TopologicalSpace α✝
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (α i)
I : Set ι
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ x ∈ closure (Set.pi I s) ↔ ∀ (i : ι), i ∈ I → x i ∈ closure (s i)
simp only [mem_closure_iff_nhdsWithin_neBot, nhdsWithin_pi_neBot]