Lightweight variant of group

[YaelDillies]

group is a very heavy tactic (it imports ring to normalise exponents) which is no more powerful than simp [mul_assoc] in many cases appearing in practice. It might be useful to have a lightweight variant of group (in the sense that it doesn't import Field or even MonoidWithZero) for those numerous cases.

Zulip

List of PRs removing uses of group:

• chore(GroupTheory/Commutator): don't import Ring #21296

[adomani]

It looks like the implementation of group involves defining (implicitly) a simp-set. Would it not be possible to define the tactic and a partial simp-set that does not require ring, and add the ring-based lemmas to the Ring file and make them part of the group simp-set?