chore(*): suggestions from the generalisation linter (#13092)
Prompted by zulip discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/An.20example.20of.20why.20formalization.20is.20useful
These are the "reasonable" suggestions from @alexjbest's generalisation linter up to `algebra.group.basic`.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
