no goals
α : Type u
β : Type v
γ : Type ?u.372393
δ : Type ?u.372396
ε : Type ?u.372399
ζ : Type ?u.372402
ι : Type u_2
π : ι → Type u_1
κ : Type ?u.372413
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
⊢ Pi.topologicalSpace = Pi.topologicalSpace
simp only [generateFrom_setOf_isOpen]