∀ {α : Type u_6} {β : Type u_7} {inst : Preorder α} {inst_1 : Preorder β} {inst_2 : MulOneClass α}
  {inst_3 : MulOneClass β} {toMonoidHom : α →* β} {monotone' : Monotone (↑toMonoidHom).toFun} {toMonoidHom_1 : α →* β}
  {monotone'_1 : Monotone (↑toMonoidHom_1).toFun},
  { toMonoidHom := toMonoidHom, monotone' := monotone' } = { toMonoidHom := toMonoidHom_1, monotone' := monotone'_1 } →
    toMonoidHom = toMonoidHom_1