refactor(algebra/group/type_tags): make additive and multiplicative structures

[gebner]

---

This is an alternative to #2292, going one step further and making the two structures instead of irreducible. I'd mainly like feedback before sinking more time into this.

I would have expected this refactoring to be more horrible. But I find that instead I can actually understand the new proofs, since they don't depend on the fact that 0 reduces to 1 or vice versa, but instead on equational lemmas that I can look at. Also equiv_rw is really helpful here.

Zulip discussion

[bryangingechen]

@gebner do you mind expanding the module doc in algebra/group/type_tags to explain how additive and multiplicative should be used now? Examples would be appreciated too. (The module doc didn't say much on this before, but I figure now is as good a time as any to request this.)

[eric-wieser]

This will need a careful merge with #6572, as that replaced section-level typeclasses with lemma-level ones.

[gebner]

This will need a careful merge with #6572, as that replaced section-level typeclasses with lemma-level ones.

I hope I didn't revert anything.

[eric-wieser]

The merge of that PR looks clean, thanks!

[bryangingechen]

The new documentation looks good to me, and the new proofs do look easier to understand as well. This is a big refactor though so I wouldn't mind getting more opinions.

[eric-wieser]

xref leanprover/lean4#777 for some discussion about the cost of making these structures.

[YaelDillies]

The discussion now pertains to mathlib4.