fix(algebra/ordered_group): remove workaround (#5103)

The problem mentioned in the TODO has been solved so the workaround is no longer needed.

src/algebra/ordered_group.lean

@@ -682,24 +682,6 @@ sub_lt_iff_lt_add'.trans (lt_add_iff_pos_left _)
 
 end ordered_add_comm_group
 
-/-
-TODO:
-The `add_lt_add_left` field of `ordered_add_comm_group` is redundant,
-and it is no longer in core so we can remove it now.
-This alternative constructor is a workaround until someone fixes this.
--/
-
-/-- Alternative constructor for ordered commutative groups,
-that avoids the field `mul_lt_mul_left`. -/
-@[to_additive "Alternative constructor for ordered commutative groups,
-that avoids the field `mul_lt_mul_left`."]
-def ordered_comm_group.mk' {α : Type u} [comm_group α] [partial_order α]
-  (mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b) :
-  ordered_comm_group α :=
-{ mul_le_mul_left := mul_le_mul_left,
-  ..(by apply_instance : comm_group α),
-  ..(by apply_instance : partial_order α) }
-
 /-- A decidable linearly ordered additive commutative group is an
 additive commutative group with a decidable linear order in which
 addition is strictly monotone. -/

src/set_theory/game.lean

@@ -157,10 +157,10 @@ def game_partial_order : partial_order game :=
   le_antisymm := le_antisymm,
   ..game.has_le }
 
-local attribute [instance] game_partial_order
-
 /-- The `<` operation provided by this `ordered_add_comm_group` is not the usual `<` on games! -/
 def ordered_add_comm_group_game : ordered_add_comm_group game :=
-ordered_add_comm_group.mk' add_le_add_left
+{ add_le_add_left := add_le_add_left,
+  ..game.add_comm_group,
+  ..game_partial_order }
 
 end game