∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] (toFun₁ toFun₂ : α → β)
  (map_sup₁ : ∀ (a b : α), toFun₁ (a ⊔ b) = toFun₁ a ⊔ toFun₁ b)
  (map_sup₂ : ∀ (a b : α), toFun₂ (a ⊔ b) = toFun₂ a ⊔ toFun₂ b),
  { toFun := toFun₁, map_sup' := map_sup₁ } ≤ { toFun := toFun₂, map_sup' := map_sup₂ } ↔ toFun₁ ≤ toFun₂