∀ {α : Type u_1} {β : Type u_2} [inst : CommSemiring α] [inst_1 : PartialOrder α] [inst_2 : Semiring β]
  [inst_3 : PartialOrder β] [IsStrictOrderedRing β] [inst_5 : Algebra α β] [SMulPosMono α β] [SMulPosReflectLE α β]
  {a₁ a₂ : α}, ((algebraMap α β) a₁ ≤ (algebraMap α β) a₂) = (a₁ ≤ a₂)