mathlib

00c39680 - refactor(set_theory/game/pgame): tweak `relabelling` definition (#14941)

refactor(set_theory/game/pgame): tweak `relabelling` definition (#14941) We simplify the definition for a `relabelling` by using `R` instead of `R.symm`. This overall leads to more symmetric proofs. We also create a constructor with the equivalences swapped. This allows us to golf various theorems. Further, we add basic API on destructuring relabellings, which makes it so that we don't have to case on them all the time.