[Merged by Bors] - feat(set_theory/{pgame, basic}): Notation for relabelling, golfing

[vihdzp]

We introduce the notation ≡r for relabellings between two pre-games. We also golf many theorems on relabellings.

---

• depends on: [Merged by Bors] - refactor(set_theory/game/nim): 0 ≈ nim 0 → nim 0 ≈ 0 #14270

I intend to use ≡ for identical pre-games (i.e. extensionally equal) at a later point.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - refactor(set_theory/game/nim): 0 ≈ nim 0 → nim 0 ≈ 0 #14270
  By Dependent Issues (🤖). Happy coding!

[vihdzp]

In the long run, we should phase out some of the equiv lemmas in favor of their relabelling counterparts. It's an analogous situation to having le lemmas alongside their lt counterparts (as in, we shouldn't do it unless in very special cases). But that can wait for another PR.

[robertylewis]

bors d+

[bors]

✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[vihdzp]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests