no goals
α : Type u_1
β : Type ?u.68647
γ : Type ?u.68650
δ : Type ?u.68653
ι : Sort u_2
κ : ι → Sort u_3
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
f : (i : ι) → κ i → Interval α
⊢ ↑(⨅ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), ↑(f i j)
simp_rw [coe_iInf]