mathlib3

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

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.