no goals
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : β ≃o γ
y : γ
⊢ IsLUB {x | (↑e ∘ f) x ≤ y} ((g ∘ ↑(OrderIso.symm e)) y)
simpa [e.le_symm_apply] using h (e.symm y)