feat(set_theory/game/pgame): ditch `restricted` (#15037)
We ditch `pgame.restricted`. The docstring erroneously claimed it to be something other than what it was, and in its current form, it really only served as a worse form of `le_def`. It was barely used anyways.
See also my comments on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Well-founded.20recursion.20for.20pgames/near/287531824).
