no goals
α✝ : Type ?u.272564
β : Type ?u.272567
γ : Type ?u.272570
δ : Type ?u.272573
inst✝¹ : TopologicalSpace α✝
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (α i)
s : (i : ι) → Set (α i)
I : Set ι
hs : ∀ (i : ι), i ∈ I → Dense (s i)
⊢ Dense (Set.pi I s)
simp only [dense_iff_closure_eq, closure_pi_set, pi_congr rfl fun i hi => (hs i hi).closure_eq,
  pi_univ]