no goals
α : Type u_1
β : Type ?u.114658
γ : Type ?u.114661
ι : Sort ?u.114664
κ : ι → Sort ?u.114669
inst✝ : CompleteLattice α
S : Set α
c : α
⊢ c ∈ Ici (sSup S) ↔ c ∈ ⨆ (a : α) (_ : a ∈ S), Ici a
simp only [mem_Ici_iff, mem_iSup_iff, sSup_le_iff]