Commit 2024-08-13 09:26 421a092f

chore(SetTheory/Game/PGame): simplify ofLists API (#15766) The equation (ofLists L R).LeftMoves = ULift (Fin L.length) (ditto for RightMoves) is entirely def-eq in Lean 4. As such, toOfListsLeftMoves doesn't solve the same problem that other toXLeftMoves equivalences do, which is provide this correspondence without having to tediously figure out how to rewrite the equality. We instead turn this into an abbreviation for ULift.up and ULift.down, which has the nice side effect of making simp much more capable of simplifying equations involving ofLists.