no goals
α : Type u_1
β : Type ?u.297838
γ : Type ?u.297841
ι : Sort ?u.297844
ι' : Sort ?u.297847
ι₂ : Sort ?u.297850
κ : ι → Sort ?u.297855
κ₁ : ι → Sort ?u.297860
κ₂ : ι → Sort ?u.297865
κ' : ι' → Sort ?u.297870
inst✝ : CompleteLattice α
s : Set α
⊢ Iic (sInf s) = ⋂ (a : α) (_ : a ∈ s), Iic a
rw [sInf_eq_iInf, Iic_iInf₂]