chore(SetTheory/Game/PGame): deprecate primed lemmas (#18469)

We perform various renames with the intent of doing away with some badly named or dubiously useful lemmas.

Author: vihdzp

Mathlib/SetTheory/Game/Basic.lean

@@ -790,10 +790,7 @@ def mulOption (x y : PGame) (i : LeftMoves x) (j : LeftMoves y) : PGame :=
   the first kind. -/
 lemma mulOption_neg_neg {x} (y) {i j} :
     mulOption x y i j = mulOption x (-(-y)) i (toLeftMovesNeg <| toRightMovesNeg j) := by
-  dsimp only [mulOption]
-  congr 2
-  · rw [neg_neg]
-  iterate 2 rw [moveLeft_neg, moveRight_neg, neg_neg]
+  simp [mulOption]
 
 /-- The left options of `x * y` agree with that of `y * x` up to equivalence. -/
 lemma mulOption_symm (x y) {i j} : ⟦mulOption x y i j⟧ = (⟦mulOption y x j i⟧ : Game) := by

Mathlib/SetTheory/Game/Impartial.lean

@@ -94,9 +94,9 @@ instance impartial_neg (G : PGame) [G.Impartial] : (-G).Impartial := by
   refine ⟨?_, fun i => ?_, fun i => ?_⟩
   · rw [neg_neg]
     exact Equiv.symm (neg_equiv_self G)
-  · rw [moveLeft_neg']
+  · rw [moveLeft_neg]
     exact impartial_neg _
-  · rw [moveRight_neg']
+  · rw [moveRight_neg]
     exact impartial_neg _
 termination_by G
 

Mathlib/SetTheory/Game/Nim.lean

@@ -84,16 +84,26 @@ theorem toRightMovesNim_symm_lt {o : Ordinal} (i : (nim o).RightMoves) :
   (toRightMovesNim.symm i).prop
 
 @[simp]
-theorem moveLeft_nim' {o : Ordinal} (i) : (nim o).moveLeft i = nim (toLeftMovesNim.symm i).val :=
+theorem moveLeft_nim {o : Ordinal} (i) : (nim o).moveLeft i = nim (toLeftMovesNim.symm i).val :=
   (congr_heq (moveLeft_nim_hEq o).symm (cast_heq _ i)).symm
 
-theorem moveLeft_nim {o : Ordinal} (i) : (nim o).moveLeft (toLeftMovesNim i) = nim i := by simp
+@[deprecated moveLeft_nim (since := "2024-10-30")]
+alias moveLeft_nim' := moveLeft_nim
+
+theorem moveLeft_toLeftMovesNim {o : Ordinal} (i) :
+    (nim o).moveLeft (toLeftMovesNim i) = nim i := by
+  simp
 
 @[simp]
-theorem moveRight_nim' {o : Ordinal} (i) : (nim o).moveRight i = nim (toRightMovesNim.symm i).val :=
+theorem moveRight_nim {o : Ordinal} (i) : (nim o).moveRight i = nim (toRightMovesNim.symm i).val :=
   (congr_heq (moveRight_nim_hEq o).symm (cast_heq _ i)).symm
 
-theorem moveRight_nim {o : Ordinal} (i) : (nim o).moveRight (toRightMovesNim i) = nim i := by simp
+@[deprecated moveRight_nim (since := "2024-10-30")]
+alias moveRight_nim' := moveRight_nim
+
+theorem moveRight_toRightMovesNim {o : Ordinal} (i) :
+    (nim o).moveRight (toRightMovesNim i) = nim i := by
+  simp
 
 /-- A recursion principle for left moves of a nim game. -/
 @[elab_as_elim]
@@ -268,7 +278,7 @@ theorem equiv_nim_grundyValue (G : PGame.{u}) [G.Impartial] :
   · rw [add_moveLeft_inr, ← Impartial.exists_left_move_equiv_iff_fuzzy_zero]
     obtain ⟨j, hj⟩ := exists_grundyValue_moveLeft_of_lt <| toLeftMovesNim_symm_lt i
     use toLeftMovesAdd (Sum.inl j)
-    rw [add_moveLeft_inl, moveLeft_nim']
+    rw [add_moveLeft_inl, moveLeft_nim]
     exact Equiv.trans (add_congr_left (equiv_nim_grundyValue _)) (hj ▸ Impartial.add_self _)
 termination_by G
 
@@ -329,7 +339,7 @@ theorem exists_grundyValue_moveRight_of_lt {G : PGame} [G.Impartial] {o : Nimber
   rw [← grundyValue_neg] at h
   obtain ⟨i, hi⟩ := exists_grundyValue_moveLeft_of_lt h
   use toLeftMovesNeg.symm i
-  rwa [← grundyValue_neg, ← moveLeft_neg']
+  rwa [← grundyValue_neg, ← moveLeft_neg]
 
 theorem grundyValue_le_of_forall_moveRight {G : PGame} [G.Impartial] {o : Nimber}
     (h : ∀ i, grundyValue (G.moveRight i) ≠ o) : G.grundyValue ≤ o := by

Mathlib/SetTheory/Game/PGame.lean

@@ -1310,34 +1310,43 @@ between them. -/
 def toRightMovesNeg {x : PGame} : x.LeftMoves ≃ (-x).RightMoves :=
   Equiv.cast (rightMoves_neg x).symm
 
-theorem moveLeft_neg {x : PGame} (i) : (-x).moveLeft (toLeftMovesNeg i) = -x.moveRight i := by
-  cases x
-  rfl
-
 @[simp]
-theorem moveLeft_neg' {x : PGame} (i) : (-x).moveLeft i = -x.moveRight (toLeftMovesNeg.symm i) := by
+theorem moveLeft_neg {x : PGame} (i) :
+    (-x).moveLeft i = -x.moveRight (toLeftMovesNeg.symm i) := by
   cases x
   rfl
 
-theorem moveRight_neg {x : PGame} (i) : (-x).moveRight (toRightMovesNeg i) = -x.moveLeft i := by
-  cases x
-  rfl
+@[deprecated moveLeft_neg (since := "2024-10-30")]
+alias moveLeft_neg' := moveLeft_neg
+
+theorem moveLeft_neg_toLeftMovesNeg {x : PGame} (i) :
+    (-x).moveLeft (toLeftMovesNeg i) = -x.moveRight i := by simp
 
 @[simp]
-theorem moveRight_neg' {x : PGame} (i) :
+theorem moveRight_neg {x : PGame} (i) :
     (-x).moveRight i = -x.moveLeft (toRightMovesNeg.symm i) := by
   cases x
   rfl
 
+@[deprecated moveRight_neg (since := "2024-10-30")]
+alias moveRight_neg' := moveRight_neg
+
+theorem moveRight_neg_toRightMovesNeg {x : PGame} (i) :
+    (-x).moveRight (toRightMovesNeg i) = -x.moveLeft i := by simp
+
+@[deprecated moveRight_neg (since := "2024-10-30")]
 theorem moveLeft_neg_symm {x : PGame} (i) :
     x.moveLeft (toRightMovesNeg.symm i) = -(-x).moveRight i := by simp
 
+@[deprecated moveRight_neg (since := "2024-10-30")]
 theorem moveLeft_neg_symm' {x : PGame} (i) :
     x.moveLeft i = -(-x).moveRight (toRightMovesNeg i) := by simp
 
+@[deprecated moveLeft_neg (since := "2024-10-30")]
 theorem moveRight_neg_symm {x : PGame} (i) :
     x.moveRight (toLeftMovesNeg.symm i) = -(-x).moveLeft i := by simp
 
+@[deprecated moveLeft_neg (since := "2024-10-30")]
 theorem moveRight_neg_symm' {x : PGame} (i) :
     x.moveRight i = -(-x).moveLeft (toLeftMovesNeg i) := by simp
 

Mathlib/SetTheory/Surreal/Multiplication.lean

@@ -119,7 +119,7 @@ lemma P2_neg_right : P2 x₁ x₂ y ↔ P2 x₁ x₂ (-y) := by
   rw [P2, P2, quot_mul_neg, quot_mul_neg, neg_inj]
 
 lemma P4_neg_left : P4 x₁ x₂ y ↔ P4 (-x₂) (-x₁) y := by
-  simp_rw [P4, PGame.neg_lt_neg_iff, moveLeft_neg', ← P3_neg]
+  simp_rw [P4, PGame.neg_lt_neg_iff, moveLeft_neg, ← P3_neg]
 
 lemma P4_neg_right : P4 x₁ x₂ y ↔ P4 x₁ x₂ (-y) := by
   rw [P4, P4, neg_neg, and_comm]
@@ -230,7 +230,7 @@ lemma ih1_swap (ih : ∀ a, ArgsRel a (Args.P1 x y) → P124 a) : IH1 y x := ih1
 lemma P3_of_ih (hy : Numeric y) (ihyx : IH1 y x) (i k l) :
     P3 (x.moveLeft i) x (y.moveLeft k) (-(-y).moveLeft l) :=
   P3_comm.2 <| ((ihyx (IsOption.moveLeft k) (isOption_neg.1 <| .moveLeft l) <| Or.inl rfl).2
-    (by rw [← moveRight_neg_symm]; apply hy.left_lt_right)).1 i
+    (by rw [moveLeft_neg, neg_neg]; apply hy.left_lt_right)).1 i
 
 lemma P24_of_ih (ihxy : IH1 x y) (i j) : P24 (x.moveLeft i) (x.moveLeft j) y :=
   ihxy (IsOption.moveLeft i) (IsOption.moveLeft j) (Or.inl rfl)
@@ -413,9 +413,8 @@ theorem P3_of_lt {y₁ y₂} (h : ∀ i, IH3 x₁ (x₂.moveLeft i) x₂ y₁ y
     P3 x₁ x₂ y₁ y₂ := by
   obtain (⟨i,hi⟩|⟨i,hi⟩) := lf_iff_exists_le.1 (lf_of_lt hl)
   · exact P3_of_le_left i (h i) hi
-  · exact P3_neg.2 <| P3_of_le_left _ (hs _) <| by
-      rw [moveLeft_neg]
-      exact neg_le_neg (le_iff_game_le.1 hi)
+  · apply P3_neg.2 <| P3_of_le_left _ (hs (toLeftMovesNeg i)) _
+    simpa
 
 /-- The main chunk of Theorem 8 in [Conway2001] / Theorem 3.8 in [SchleicherStoll]. -/
 theorem main (a : Args) : a.Numeric → P124 a := by
@@ -488,7 +487,7 @@ theorem P3_of_lt_of_lt (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy₁ : y
   · have hi := hx₁.neg.moveLeft i
     exact ⟨(P24 hx₂.neg hi hy₁).1, (P24 hx₂.neg hi hy₂).1,
       P3_comm.2 <| ((P24 hy₁ hy₂ hx₁).2 hy).2 _, by
-        rw [moveLeft_neg', ← P3_neg, neg_lt_neg_iff]
+        rw [moveLeft_neg, ← P3_neg, neg_lt_neg_iff]
         exact ih _ (fst <| IsOption.moveRight _) (hx₁.moveRight _) hx₂⟩
 
 theorem Numeric.mul_pos (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hp₁ : 0 < x₁) (hp₂ : 0 < x₂) :