mathlib3

60897e3b - refactor(set_theory/game/nim): `0 ≈ nim 0` → `nim 0 ≈ 0` (#14270)

refactor(set_theory/game/nim): `0 ≈ nim 0` → `nim 0 ≈ 0` (#14270) We invert the directions of a few simple equivalences/relabellings to a more natural order (simpler on the RHS).