no goals
α : Type u_2
β : Type u_1
β₂ : Type ?u.79767
γ : Type ?u.79770
ι : Sort u_3
ι' : Sort ?u.79776
κ : ι → Sort ?u.79781
κ' : ι' → Sort ?u.79786
inst✝¹ : CompleteLattice α
f✝ g s t : ι → α
a b : α
inst✝ : CompleteLattice β
f : α ≃o β
x✝ : ι → α
x : α
⊢ ↑f (⨆ (i : ι), x✝ i) ≤ ↑f x ↔ (⨆ (i : ι), ↑f (x✝ i)) ≤ ↑f x
simp only [f.le_iff_le, iSup_le_iff]