no goals
α : Type u_1
β : Type ?u.69615
γ : Type ?u.69618
ι : Sort u_2
κ : ι → Sort ?u.69626
inst✝ : LE α
S : Set (LowerSet α)
s t : LowerSet α
a : α
f : ι → LowerSet α
⊢ ↑(⨆ (i : ι), f i) = ⋃ (i : ι), ↑(f i)
simp_rw [iSup, coe_sSup, mem_range, iUnion_exists, iUnion_iUnion_eq']