∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedMonoid α],
  UpperSet.instCommMonoid =
    { toSemigroup := UpperSet.commSemigroup.toSemigroup, toOne := UpperSet.instOne, one_mul := ⋯, mul_one := ⋯,
      npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }