no goals
α : Type u_1
β : Type ?u.120495
γ : Type ?u.120498
ι : Sort ?u.120501
κ : ι → Sort ?u.120506
inst✝ : CompleteLattice α
S : Set α
c : α
⊢ c ∈ Iic (sInf S) ↔ c ∈ ⨅ (a : α) (_ : a ∈ S), Iic a
simp only [mem_Iic_iff, mem_iInf₂_iff, le_sInf_iff]