no goals
α : Type u_1
β : Type ?u.115407
γ : Type ?u.115410
ι : Sort u_2
κ : ι → Sort ?u.115418
inst✝ : CompleteLattice α
f : ι → α
c : α
⊢ c ∈ Ici (⨆ (i : ι), f i) ↔ c ∈ ⨆ (i : ι), Ici (f i)
simp only [mem_Ici_iff, mem_iSup_iff, iSup_le_iff]