no goals
α✝ : Type u
β : Type v
ι✝ : Sort w
γ : Type x
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝⁴ : Finite ι
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1
inst✝ : Order.Frame α
f : ι → ι' → α
hf : ∀ (i : ι), Monotone (f i)
⊢ (⨆ (j : ι'), ⨅ (i : ι), f i j) = ⨅ (i : ι), ⨆ (j : ι'), f i j
simpa only [iInf_univ] using finite_univ.iSup_biInf_of_monotone fun i _ => hf i