no goals
α : Type u_1
β : Type ?u.295745
γ : Type ?u.295748
ι : Sort u_2
ι' : Sort ?u.295754
ι₂ : Sort ?u.295757
κ : ι → Sort ?u.295762
κ₁ : ι → Sort ?u.295767
κ₂ : ι → Sort ?u.295772
κ' : ι' → Sort ?u.295777
inst✝ : CompleteLattice α
f : ι → α
x✝ : α
⊢ x✝ ∈ Iic (⨅ (i : ι), f i) ↔ x✝ ∈ ⋂ (i : ι), Iic (f i)
simp only [mem_Iic, le_iInf_iff, mem_iInter]