feat(set_theory/game/pgame): Empty instances (#13635)

src/set_theory/game/pgame.lean

@@ -193,6 +193,9 @@ instance : has_zero pgame := ⟨⟨pempty, pempty, pempty.elim, pempty.elim⟩
 @[simp] lemma zero_left_moves : (0 : pgame).left_moves = pempty := rfl
 @[simp] lemma zero_right_moves : (0 : pgame).right_moves = pempty := rfl
 
+instance is_empty_zero_left_moves : is_empty (0 : pgame).left_moves := pempty.is_empty
+instance is_empty_zero_right_moves : is_empty (0 : pgame).right_moves := pempty.is_empty
+
 instance : inhabited pgame := ⟨0⟩
 
 /-- The pre-game `one` is defined by `1 = { 0 | }`. -/
@@ -202,6 +205,8 @@ instance : has_one pgame := ⟨⟨punit, pempty, λ _, 0, pempty.elim⟩⟩
 @[simp] lemma one_move_left : (1 : pgame).move_left punit.star = 0 := rfl
 @[simp] lemma one_right_moves : (1 : pgame).right_moves = pempty := rfl
 
+instance is_empty_one_right_moves : is_empty (1 : pgame).right_moves := pempty.is_empty
+
 /-- Define simultaneously by mutual induction the `<=` and `<`
   relation on pre-games. The ZFC definition says that `x = {xL | xR}`
   is less or equal to `y = {yL | yR}` if `∀ x₁ ∈ xL, x₁ < y`