refactor(set_theory/game/*): Delete `winner.lean` (#14271)
The file `winner.lean` currently consists of one-line definitions and theorems, including aliases for basic inequalities. This PR removes the file, inlines all previous definitions and theorems, and golfs various proofs in the process.
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
