chore(set_theory/pgame): add protected (#9022)

Breaks #7843 into smaller PRs.

These lemmas about `pgame` conflict with the ones for `game` when used in `calc` mode proofs, which confuses Lean.
There is no way to use the lemmas for `game` (required for surreal numbers) without using `_root_` as `game` inherits these lemmas from its abelian group structure.

Author: apurvnakade

src/set_theory/game/impartial.lean

@@ -138,11 +138,11 @@ begin
     split,
     { rw le_iff_sub_nonneg,
       exact le_trans hGHp.2
-        (le_trans add_comm_le $ le_of_le_of_equiv (le_refl _) $ add_congr (equiv_refl _)
+        (le_trans add_comm_le $ le_of_le_of_equiv (pgame.le_refl _) $ add_congr (equiv_refl _)
         (neg_equiv_self G)) },
     { rw le_iff_sub_nonneg,
       exact le_trans hGHp.2
-        (le_of_le_of_equiv (le_refl _) $ add_congr (equiv_refl _) (neg_equiv_self H)) } }
+        (le_of_le_of_equiv (pgame.le_refl _) $ add_congr (equiv_refl _) (neg_equiv_self H)) } }
 end
 
 lemma le_zero_iff {G : pgame} [G.impartial] : G ≤ 0 ↔ 0 ≤ G :=

src/set_theory/game/winner.lean

@@ -74,7 +74,7 @@ lemma not_first_wins_of_first_loses {G : pgame} : G.first_loses → ¬G.first_wi
 begin
   rw first_loses_is_zero,
   rintros h ⟨h₀, -⟩,
-  exact lt_irrefl 0 (lt_of_lt_of_equiv h₀ h)
+  exact pgame.lt_irrefl 0 (lt_of_lt_of_equiv h₀ h)
 end
 
 lemma not_first_loses_of_first_wins {G : pgame} : G.first_wins → ¬G.first_loses :=

src/set_theory/pgame.lean

@@ -359,15 +359,15 @@ end
 theorem not_le {x y : pgame} : ¬ x ≤ y ↔ y < x := not_le_lt.1
 theorem not_lt {x y : pgame} : ¬ x < y ↔ y ≤ x := not_le_lt.2
 
-@[refl] theorem le_refl : ∀ x : pgame, x ≤ x
+@[refl] protected theorem le_refl : ∀ x : pgame, x ≤ x
 | ⟨l, r, L, R⟩ := by rw mk_le_mk; exact
 ⟨λ i, lt_mk_of_le (le_refl _), λ i, mk_lt_of_le (le_refl _)⟩
 
-theorem lt_irrefl (x : pgame) : ¬ x < x :=
-not_lt.2 (le_refl _)
+protected theorem lt_irrefl (x : pgame) : ¬ x < x :=
+not_lt.2 (pgame.le_refl _)
 
-theorem ne_of_lt : ∀ {x y : pgame}, x < y → x ≠ y
-| x _ h rfl := lt_irrefl x h
+protected theorem ne_of_lt : ∀ {x y : pgame}, x < y → x ≠ y
+| x _ h rfl := pgame.lt_irrefl x h
 
 theorem le_trans_aux
   {xl xr} {xL : xl → pgame} {xR : xr → pgame}
@@ -415,7 +415,7 @@ def equiv (x y : pgame) : Prop := x ≤ y ∧ y ≤ x
 
 local infix ` ≈ ` := pgame.equiv
 
-@[refl, simp] theorem equiv_refl (x) : x ≈ x := ⟨le_refl _, le_refl _⟩
+@[refl, simp] theorem equiv_refl (x) : x ≈ x := ⟨pgame.le_refl _, pgame.le_refl _⟩
 @[symm] theorem equiv_symm {x y} : x ≈ y → y ≈ x | ⟨xy, yx⟩ := ⟨yx, xy⟩
 @[trans] theorem equiv_trans {x y z} : x ≈ y → y ≈ z → x ≈ z
 | ⟨xy, yx⟩ ⟨yz, zy⟩ := ⟨le_trans xy yz, le_trans zy yx⟩