mathlib3

4bfae3d8 - feat(set_theory/game/pgame): remove nolint (#13680)

feat(set_theory/game/pgame): remove nolint (#13680) We remove `@[nolint has_inhabited_instance]` from `left_moves` and `right_moves` by providing the appropriate instances for `star`.