no goals
α : Type ?u.306093
β : Type u_1
γ : Type ?u.306099
ι : Sort ?u.306102
ι' : Sort ?u.306105
ι₂ : Sort ?u.306108
κ : ι → Sort ?u.306113
κ₁ : ι → Sort ?u.306118
κ₂ : ι → Sort ?u.306123
κ' : ι' → Sort ?u.306128
inst✝ : CompleteLattice β
s : Set (Set β)
⊢ sSup (⋃₀ s) = ⨆ (t : Set β) (_ : t ∈ s), sSup t
simp only [sUnion_eq_biUnion, sSup_eq_iSup, iSup_iUnion]