no goals
α : Type u_1
β : Type ?u.297530
γ : Type ?u.297533
ι : Sort ?u.297536
ι' : Sort ?u.297539
ι₂ : Sort ?u.297542
κ : ι → Sort ?u.297547
κ₁ : ι → Sort ?u.297552
κ₂ : ι → Sort ?u.297557
κ' : ι' → Sort ?u.297562
inst✝ : CompleteLattice α
s : Set α
⊢ Ici (sSup s) = ⋂ (a : α) (_ : a ∈ s), Ici a
rw [sSup_eq_iSup, Ici_iSup₂]