∀ {G : Type u_1} {H : Type u_2} [inst : AddCommMonoid G] [inst_1 : PartialOrder G] [inst_2 : AddCommMonoid H]
  [inst_3 : PartialOrder H] (e : Multiplicative G ≃*o Multiplicative H),
  (fun e => { toMulEquiv := AddEquiv.toMultiplicative ↑e, map_le_map_iff' := ⋯ })
      ((fun e => { toAddEquiv := AddEquiv.toMultiplicative.symm ↑e, map_le_map_iff' := ⋯ }) e) =
    e