no goals
ι✝ : Type ?u.17100
α : Type u_2
β : Type ?u.17106
γ : Type ?u.17109
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Sort u_1
s : ι → Opens α
⊢ ↑(⨆ (i : ι), s i) = ⋃ (i : ι), ↑(s i)
simp [iSup]