chore(algebra/group/defs): Remove shortcut instance definitions (#4955)

This means that `group.to_left_cancel_semigroup` is now spelt `group.to_cancel_monoid.to_left_cancel_monoid.to_left_cancel_semigroup`.
The longer spelling shouldn't actually matter because type inference will do it anyway.

I don't know whether this matters, but this should slightly reduce the number of connections that instance resolution must check.

This shortcut wasn't added deliberately, it seems it just got added accidentally when #3688 was introduced.

src/algebra/group/defs.lean

@@ -333,20 +333,11 @@ lemma mul_inv_cancel_right (a b : G) : a * b * b⁻¹ = a :=
 by rw [mul_assoc, mul_right_inv, mul_one]
 
 @[priority 100, to_additive]    -- see Note [lower instance priority]
-instance group.to_left_cancel_semigroup : left_cancel_semigroup G :=
-{ mul_left_cancel := λ a b c h, by rw [← inv_mul_cancel_left a b, h, inv_mul_cancel_left],
-  ..‹group G› }
-
-@[priority 100, to_additive]    -- see Note [lower instance priority]
-instance group.to_right_cancel_semigroup : right_cancel_semigroup G :=
+instance group.to_cancel_monoid : cancel_monoid G :=
 { mul_right_cancel := λ a b c h, by rw [← mul_inv_cancel_right a b, h, mul_inv_cancel_right],
+  mul_left_cancel := λ a b c h, by rw [← inv_mul_cancel_left a b, h, inv_mul_cancel_left],
   ..‹group G› }
 
-@[priority 100, to_additive]    -- see Note [lower instance priority]
-instance group.to_cancel_monoid : cancel_monoid G :=
-{ ..‹group G›, .. group.to_left_cancel_semigroup,
-  ..group.to_right_cancel_semigroup }
-
 end group
 
 section add_group
@@ -382,7 +373,6 @@ variables {G : Type u} [comm_group G]
 @[priority 100, to_additive]    -- see Note [lower instance priority]
 instance comm_group.to_cancel_comm_monoid : cancel_comm_monoid G :=
 { ..‹comm_group G›,
-  ..group.to_left_cancel_semigroup,
-  ..group.to_right_cancel_semigroup }
+  ..group.to_cancel_monoid }
 
 end comm_group