chore(set_theory/game/nim): review simp lemmas (#15407)

This PR does the following:
- Untag `grundy_value_eq_iff_equiv_nim`, `grundy_value_eq_iff_equiv`, and `grundy_value_iff_equiv_zero` as `simp`, since it's sometimes easier to directly prove the equality of Grundy values than it is the equivalence of games. 
- Untag `nim_zero_equiv` and `nim_one_equiv` as `simp` - since equivalences can't be used to rewrite, these are nearly useless as `simp` lemmas.
- Tag `nim.grundy_value` and `grundy_value_star` as `simp`.

src/set_theory/game/nim.lean

@@ -115,7 +115,7 @@ by { rw nim_def, exact ordinal.unique_out_one }
 /-- `nim 0` has exactly the same moves as `0`. -/
 def nim_zero_relabelling : nim 0 ≡r 0 := relabelling.is_empty _
 
-@[simp] theorem nim_zero_equiv : nim 0 ≈ 0 := equiv.is_empty _
+theorem nim_zero_equiv : nim 0 ≈ 0 := equiv.is_empty _
 
 /-- `nim 1` has exactly the same moves as `star`. -/
 noncomputable def nim_one_relabelling : nim 1 ≡r star :=
@@ -126,7 +126,7 @@ begin
   all_goals { simp, exact nim_zero_relabelling }
 end
 
-@[simp] theorem nim_one_equiv : nim 1 ≈ star := nim_one_relabelling.equiv
+theorem nim_one_equiv : nim 1 ≈ star := nim_one_relabelling.equiv
 
 @[simp] lemma nim_birthday (o : ordinal) : (nim o).birthday = o :=
 begin
@@ -243,24 +243,26 @@ begin
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
-@[simp] lemma grundy_value_eq_iff_equiv_nim (G : pgame) [G.impartial] (o : ordinal) :
+lemma grundy_value_eq_iff_equiv_nim {G : pgame} [G.impartial] {o : ordinal} :
   grundy_value G = o ↔ G ≈ nim o :=
 ⟨by { rintro rfl, exact equiv_nim_grundy_value G },
   by { intro h, rw ←nim.equiv_iff_eq, exact (equiv_nim_grundy_value G).symm.trans h }⟩
 
-lemma nim.grundy_value (o : ordinal.{u}) : grundy_value (nim o) = o :=
-by simp
+@[simp] lemma nim.grundy_value (o : ordinal.{u}) : grundy_value (nim o) = o :=
+grundy_value_eq_iff_equiv_nim.2 pgame.equiv_rfl
 
-@[simp] lemma grundy_value_eq_iff_equiv (G H : pgame) [G.impartial] [H.impartial] :
+lemma grundy_value_eq_iff_equiv (G H : pgame) [G.impartial] [H.impartial] :
   grundy_value G = grundy_value H ↔ G ≈ H :=
-(grundy_value_eq_iff_equiv_nim _ _).trans (equiv_congr_left.1 (equiv_nim_grundy_value H) _).symm
+grundy_value_eq_iff_equiv_nim.trans (equiv_congr_left.1 (equiv_nim_grundy_value H) _).symm
 
-@[simp] lemma grundy_value_zero : grundy_value 0 = 0 := by simp [nim.nim_zero_equiv.symm]
+@[simp] lemma grundy_value_zero : grundy_value 0 = 0 :=
+grundy_value_eq_iff_equiv_nim.2 nim.nim_zero_equiv.symm
 
-@[simp] lemma grundy_value_iff_equiv_zero (G : pgame) [G.impartial] : grundy_value G = 0 ↔ G ≈ 0 :=
+lemma grundy_value_iff_equiv_zero (G : pgame) [G.impartial] : grundy_value G = 0 ↔ G ≈ 0 :=
 by rw [←grundy_value_eq_iff_equiv, grundy_value_zero]
 
-lemma grundy_value_star : grundy_value star = 1 := by simp [nim.nim_one_equiv.symm]
+@[simp] lemma grundy_value_star : grundy_value star = 1 :=
+grundy_value_eq_iff_equiv_nim.2 nim.nim_one_equiv.symm
 
 @[simp] lemma grundy_value_nim_add_nim (n m : ℕ) :
   grundy_value (nim.{u} n + nim.{u} m) = nat.lxor n m :=