mathlib3

dc9e5ba6 - chore(set_theory/game/pgame): golf le and lf basic API (#18498)

chore(set_theory/game/pgame): golf le and lf basic API (#18498) Co-authored-by: Violeta Hernández [vi.hdz.p@gmail.com](mailto:vi.hdz.p@gmail.com) Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>