mathlib

df64e5e5 - chore(set_theory/game/pgame): minor golf (#14171)