mathlib3

3c7394fe - fix(group_theory/*, algebra/group): [to_additive, simp] doesn't work (#5468)

fix(group_theory/*, algebra/group): [to_additive, simp] doesn't work (#5468) As explained in `algebra/group/to_additive`, `@[to_additive, simp]` doesn't work (it doesn't attach a `simp` attribute to the additive lemma), but conversely `@[simps, to_additive]` is also wrong. Along the way I also noticed that some `right_inv` (as in an inverse function) lemmas were being changed to `right_neg` by to_additive :D