Commit 2025-01-28 02:20 022b2bf3
View on Github →feat(SetTheory/Game/PGame): rewrite left moves of -x as right moves of x under binders (#21109)
These lemmas strengthen our simp set considerably, and allow us to now prove various other theorems by simp on the negative game.
See Zulip for some discussion on this.