no goals
α : Type u_1
β : Type ?u.296897
γ : Type ?u.296900
ι : Sort u_2
ι' : Sort ?u.296906
ι₂ : Sort ?u.296909
κ : ι → Sort u_3
κ₁ : ι → Sort ?u.296919
κ₂ : ι → Sort ?u.296924
κ' : ι' → Sort ?u.296929
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Iic (⨅ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), Iic (f i j)
simp_rw [Iic_iInf]