mathlib3

7c6cd38b - chore(set_theory/game/pgame): remove weird `simp` lemma (#14954)

chore(set_theory/game/pgame): remove weird `simp` lemma (#14954) I added this back before there was much API on casting natural numbers to pre-games, as a safeguard in case I used the wrong `1`. In retrospective this theorem was kind of dumb.