no goals
α : Type u_1
β : Type ?u.65135
γ : Type ?u.65138
δ : Type ?u.65141
ι : Sort u_2
κ : ι → Sort ?u.65149
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
f : ι → Interval α
⊢ ↑(⨅ (i : ι), f i) = ⋂ (i : ι), ↑(f i)
simp [iInf]