mathlib3

4b788397 - feat(set_theory/game/basic): generalize equivalences to relabellings (#15252)

feat(set_theory/game/basic): generalize equivalences to relabellings (#15252) This PR does the following: - Generalize `quot_mul_comm`, `quot_neg_mul`, `quot_mul_neg`, `quot_mul_one`, `quot_one_mul` from pre-game equivalences to relabellings. - Add a bunch of `dsimp` lemmas, used in `neg_mul_relabelling`. - Heavily golf the corresponding proofs. - Uncontroversial spacing and parentheses fixes.