From 855fd1cd36e6fd669585891e6d12fa93995b3eb1 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 1 Mar 2023 02:24:27 +0800
Subject: [PATCH 01/22] feat(set_theory/game/pgame): define `pgame.identical`

---
 src/set_theory/game/pgame.lean | 286 ++++++++++++++++++++++++++++++++-
 1 file changed, 285 insertions(+), 1 deletion(-)

diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index 3c9a085d0633f..39fc90293e68c 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -21,7 +21,7 @@ types (thought of as indexing the possible moves for the players Left and Right)
 functions out of these types to `pgame` (thought of as describing the resulting game after making a
 move).
 
-Combinatorial games themselves, as a quotient of pregames, are constructed in `game.lean`.
+Combinatorial games themselves, as a quotient of pregames, are constructed in `basic.lean`.
 
 ## Conway induction
 
@@ -672,6 +672,140 @@ begin
   exact lt_or_equiv_or_gt_or_fuzzy x y
 end
 
+end pgame
+
+-- This can also used for golf `Set.equiv` lemmas, but I'm not sure where to put it.
+/-- An auxiliary definition for `pgame.identical` -/
+def forall_exists_rel {ι₁ ι₂ α₁ α₂ : Type*} (r : α₁ → α₂ → Prop) (s : ι₁ → α₁) (t : ι₂ → α₂) :=
+  (∀ i, ∃ j, r (s i) (t j)) ∧ (∀ j, ∃ i, r (s i) (t j))
+
+namespace forall_exists_rel
+variables {ι₁ ι₂ ι₃ α₁ α₂ α₃ : Type*}
+
+lemma refl {r : α₁ → α₁ → Prop} (s : ι₁ → α₁) (hr : ∀ i, r (s i) (s i)) :
+  forall_exists_rel r s s :=
+⟨λ i, ⟨i, hr _⟩, λ i, ⟨i, hr _⟩⟩
+
+lemma euc {r₁₂ : α₁ → α₂ → Prop} {r₃₂ : α₃ → α₂ → Prop} {r₁₃ : α₁ → α₃ → Prop}
+  {s : ι₁ → α₁} {t : ι₂ → α₂} {u : ι₃ → α₃}
+  (hr : ∀ i j k, r₁₂ (s i) (t j) → r₃₂ (u k) (t j) → r₁₃ (s i) (u k)) :
+  forall_exists_rel r₁₂ s t → forall_exists_rel r₃₂ u t → forall_exists_rel r₁₃ s u :=
+λ h₁ h₂, ⟨λ i, let ⟨j, hj⟩ := h₁.1 i , ⟨k, hk⟩ := h₂.2 j in ⟨k, hr _ _ _ hj hk⟩,
+  λ k, let ⟨j, hj⟩ := h₂.1 k, ⟨i, hi⟩ := h₁.2 j in ⟨i, hr _ _ _ hi hj⟩⟩
+
+lemma symm {r₁₂ : α₁ → α₂ → Prop} {r₂₁ : α₂ → α₁ → Prop}
+  {s : ι₁ → α₁} {t : ι₂ → α₂} (hr : ∀ i j, r₁₂ (s i) (t j) → r₂₁ (t j) (s i)) :
+  forall_exists_rel r₁₂ s t → forall_exists_rel r₂₁ t s :=
+λ h, ⟨λ i, (h.2 i).imp (λ _, hr _ _), λ i, (h.1 i).imp (λ _, hr _ _)⟩
+
+lemma trans {r₁₂ : α₁ → α₂ → Prop} {r₂₃ : α₂ → α₃ → Prop} {r₁₃ : α₁ → α₃ → Prop}
+  {s : ι₁ → α₁} {t : ι₂ → α₂} {u : ι₃ → α₃}
+  (hr : ∀ i j k, r₁₂ (s i) (t j) → r₂₃ (t j) (u k) → r₁₃ (s i) (u k)) :
+  forall_exists_rel r₁₂ s t → forall_exists_rel r₂₃ t u → forall_exists_rel r₁₃ s u :=
+λ h₁ h₂, ⟨λ i, let ⟨j, hj⟩ := h₁.1 i, ⟨k, hk⟩ := h₂.1 j in ⟨k, hr _ _ _ hj hk⟩,
+  λ k, let ⟨j, hj⟩ := h₂.2 k, ⟨i, hi⟩ := h₁.2 j in ⟨i, hr _ _ _ hi hj⟩⟩
+
+end forall_exists_rel
+
+namespace pgame
+open_locale pgame
+
+def identical : Π (x y : pgame), Prop
+| (mk _ _ xL xR) (mk _ _ yL yR) :=
+  ((∀ i, ∃ j, identical (xL i) (yL j)) ∧ (∀ j, ∃ i, identical (xL i) (yL j))) ∧
+    ((∀ i, ∃ j, identical (xR i) (yR j)) ∧ (∀ j, ∃ i, identical (xR i) (yR j)))
+
+localized "infix (name := pgame.identical) ` ≡ `:50 := pgame.identical" in pgame
+
+def memₗ (x y : pgame.{u}) : Prop := ∃ b, x ≡ (y.move_left b)
+def memᵣ (x y : pgame.{u}) : Prop := ∃ b, x ≡ (y.move_right b)
+
+localized "infix (name := pgame.memₗ) ` ∈ₗ `:50 := pgame.memₗ" in pgame
+localized "infix (name := pgame.memᵣ) ` ∈ᵣ `:50 := pgame.memᵣ" in pgame
+
+theorem identical_iff' : Π {x y : pgame}, identical x y ↔
+  forall_exists_rel (≡) x.move_left y.move_left ∧
+    forall_exists_rel (≡) x.move_right y.move_right
+| (mk _ _ _ _) (mk _ _ _ _) := iff.rfl
+
+@[refl] protected theorem identical.refl (x) : x ≡ x :=
+pgame.rec_on x $ λ l r L R IHL IHR, ⟨forall_exists_rel.refl _ IHL, forall_exists_rel.refl _ IHR⟩
+
+protected theorem identical.rfl : ∀ {x}, x ≡ x := identical.refl
+
+@[trans] protected theorem identical.euc {x} : ∀ {y z}, x ≡ y → z ≡ y → x ≡ z :=
+pgame.rec_on x $ λ xl xr xL xR IHL IHR y, pgame.cases_on y $ λ yl yr yL yR ⟨zl, zr, zL, zR⟩
+  ⟨hL₁, hR₁⟩ ⟨hL₂, hR₂⟩, ⟨forall_exists_rel.euc (λ _ _ _, IHL _) hL₁ hL₂,
+  forall_exists_rel.euc (λ _ _ _, IHR _) hR₁ hR₂⟩
+
+@[symm] protected theorem identical.symm {x y} : x ≡ y → y ≡ x :=
+(identical.refl y).euc
+
+protected theorem identical.comm {x y} : x ≡ y ↔ y ≡ x :=
+⟨identical.symm, identical.symm⟩
+
+@[trans] protected theorem identical.trans {x y z} (h₁ : x ≡ y) (h₂ : y ≡ z) : x ≡ z :=
+h₁.euc h₂.symm
+
+theorem identical_of_is_empty (x y : pgame)
+  [is_empty x.left_moves] [is_empty x.right_moves]
+  [is_empty y.left_moves] [is_empty y.right_moves] : identical x y :=
+identical_iff'.2 $ by simp [forall_exists_rel]
+
+def identical_setoid : setoid pgame :=
+⟨identical, identical.refl, λ x y, identical.symm, λ x y z, identical.trans⟩
+
+instance : is_refl pgame (≡) := ⟨identical.refl⟩
+instance : is_symm pgame (≡) := ⟨λ _ _, identical.symm⟩
+instance : is_trans pgame (≡) := ⟨λ _ _ _, identical.trans⟩
+instance : is_equiv pgame (≡) := { }
+
+lemma identical.le {x} : ∀ {y}, x ≡ y → x ≤ y :=
+pgame.rec_on x $ λ xl xr xL xR IHL IHR ⟨yl, yr, yL, yR⟩ ⟨hL, hR⟩, le_of_forall_lf
+  (λ i, let ⟨j, hj⟩ := hL.1 i in lf_of_le_move_left (IHL _ hj))
+  (λ i, let ⟨j, hj⟩ := hR.2 i in lf_of_move_right_le (IHR _ hj))
+
+lemma identical.trans_eq {x y z} (h₁ : x ≡ y) (h₂ : y = z) : x ≡ z := h₁.trans (of_eq h₂)
+
+lemma identical.equiv {x y} (h : x ≡ y) : x ≈ y := ⟨h.le, h.symm.le⟩
+
+theorem identical_iff : Π {x y : pgame}, x ≡ y ↔
+  ((∀ i, (x.move_left i) ∈ₗ y) ∧ (∀ j, (y.move_left j) ∈ₗ x)) ∧
+    ((∀ i, (x.move_right i) ∈ᵣ y) ∧ (∀ j, (y.move_right j) ∈ᵣ x))
+| (mk _ _ _ _) (mk _ _ _ _) := begin
+  convert identical_iff';
+  exact pi_congr (λ i, propext (exists_congr $ λ j, by rw [identical.comm])),
+end
+
+theorem memₗ.congr_right : Π {x y : pgame.{u}},
+  x ≡ y → (∀ {w : pgame.{u}}, w ∈ₗ x ↔ w ∈ₗ y)
+| (mk _ _ xL xR) (mk _ _ yL yR) ⟨⟨h₁, h₂⟩, _⟩ w :=
+  ⟨λ ⟨i, hi⟩, (h₁ i).imp (λ _, hi.trans), λ ⟨j, hj⟩, (h₂ j).imp (λ i hi, hj.trans hi.symm)⟩
+
+theorem memᵣ.congr_right : Π {x y : pgame.{u}},
+  x ≡ y → (∀ {w : pgame.{u}}, w ∈ᵣ x ↔ w ∈ᵣ y)
+| (mk _ _ xL xR) (mk _ _ yL yR) ⟨_, ⟨h₁, h₂⟩⟩ w :=
+  ⟨λ ⟨i, hi⟩, (h₁ i).imp (λ _, hi.trans), λ ⟨j, hj⟩, (h₂ j).imp (λ i hi, hj.trans hi.symm)⟩
+
+theorem memₗ.congr_left : Π {x y : pgame.{u}},
+  x ≡ y → (∀ {w : pgame.{u}}, x ∈ₗ w ↔ y ∈ₗ w)
+| x y h (mk _ _ L R) := ⟨λ ⟨i, hi⟩, ⟨i, h.symm.trans hi⟩, λ ⟨i, hi⟩, ⟨i, h.trans hi⟩⟩
+
+theorem memᵣ.congr_left : Π {x y : pgame.{u}},
+  x ≡ y → (∀ {w : pgame.{u}}, x ∈ᵣ w ↔ y ∈ᵣ w)
+| x y h (mk _ _ L R) := ⟨λ ⟨i, hi⟩, ⟨i, h.symm.trans hi⟩, λ ⟨i, hi⟩, ⟨i, h.trans hi⟩⟩
+
+lemma identical.ext : ∀ {x y} (hl : ∀ z, z ∈ₗ x ↔ z ∈ₗ y) (hr : ∀ z, z ∈ᵣ x ↔ z ∈ᵣ y), x ≡ y
+| (mk _ _ xL xR) (mk _ _ yL yR) hl hr := identical_iff.mpr
+  ⟨⟨λ i, (hl _).mp ⟨i, refl _⟩, λ j, (hl _).mpr ⟨j, refl _⟩⟩,
+    ⟨λ i, (hr _).mp ⟨i, refl _⟩, λ j, (hr _).mpr ⟨j, refl _⟩⟩⟩
+
+lemma identical.congr_right {x y z} (h : x ≡ y) : z ≡ x ↔ z ≡ y :=
+⟨λ hz, hz.trans h, λ hz, hz.trans h.symm⟩
+
+lemma identical.congr_left {x y z} (h : x ≡ y) : x ≡ z ↔ y ≡ z :=
+⟨λ hz, h.symm.trans hz, λ hz, h.trans hz⟩
+
 /-! ### Relabellings -/
 
 /--
@@ -902,6 +1036,30 @@ lemma move_right_neg_symm' {x : pgame} (i) :
   x.move_right i = -(-x).move_left (to_left_moves_neg i) :=
 by simp
 
+lemma memₗ_neg_iff : Π {x y : pgame},
+  x ∈ₗ -y ↔ (∃ i, x ≡ -(y.move_right i))
+| (mk xl xr xL xR) (mk yl yr yL yR) := iff.rfl
+
+lemma memᵣ_neg_iff : Π {x y : pgame},
+  x ∈ᵣ -y ↔ (∃ i, x ≡ -(y.move_left i))
+| (mk xl xr xL xR) (mk yl yr yL yR) := iff.rfl
+
+lemma identical.neg : Π {x₁ x₂ : pgame.{u}} (hx : x₁ ≡ x₂), -x₁ ≡ -x₂
+| (mk x₁l x₁r x₁L x₁R) (mk x₂l x₂r x₂L x₂R) ⟨⟨hL₁, hL₂⟩, ⟨hR₁, hR₂⟩⟩ :=
+  ⟨⟨λ i, (hR₁ i).imp (λ j, identical.neg), λ j, (hR₂ j).imp (λ i, identical.neg)⟩,
+    ⟨λ i, (hL₁ i).imp (λ j, identical.neg), λ j, (hL₂ j).imp (λ i, identical.neg)⟩⟩
+using_well_founded { dec_tac := pgame_wf_tac }
+
+lemma memₗ_neg_iff' : Π {x y : pgame},
+  x ∈ₗ -y ↔ (∃ z ∈ᵣ y, x ≡ -z)
+| (mk xl xr xL xR) (mk yl yr yL yR) := memₗ_neg_iff.trans
+  ⟨λ ⟨i, hi⟩, ⟨_, ⟨_, refl _⟩, hi⟩, λ ⟨_, ⟨i, hi⟩, h⟩, ⟨i, h.trans hi.neg⟩⟩
+
+lemma memᵣ_neg_iff' : Π {x y : pgame},
+  x ∈ᵣ -y ↔ (∃ z ∈ₗ y, x ≡ -z)
+| (mk xl xr xL xR) (mk yl yr yL yR) := memᵣ_neg_iff.trans
+  ⟨λ ⟨i, hi⟩, ⟨_, ⟨_, refl _⟩, hi⟩, λ ⟨_, ⟨i, hi⟩, h⟩, ⟨i, h.trans hi.neg⟩⟩
+
 /-- If `x` has the same moves as `y`, then `-x` has the sames moves as `-y`. -/
 def relabelling.neg_congr : ∀ {x y : pgame}, x ≡r y → -x ≡r -y
 | ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ ⟨L, R, hL, hR⟩ :=
@@ -1130,6 +1288,132 @@ instance is_empty_nat_right_moves : ∀ n : ℕ, is_empty (right_moves n)
   apply_instance
 end
 
+lemma memₗ_add_iff : Π {x y₁ y₂ : pgame},
+  x ∈ₗ y₁ + y₂ ↔ (∃ i, x ≡ (y₁.move_left i) + y₂) ∨ (∃ i, x ≡ y₁ + (y₂.move_left i))
+| (mk x₁l x₁r x₁L x₁R) (mk x₂l x₂r x₂L x₂R) (mk yl yr yL yR) := begin
+  constructor,
+  { rintros ⟨(i | i), hi⟩, exacts [or.inl ⟨_, hi⟩, or.inr ⟨_, hi⟩], },
+  { rintros (⟨i, h⟩ | ⟨i, h⟩), exacts [⟨sum.inl i, h⟩, ⟨sum.inr i, h⟩], },
+end
+
+lemma memᵣ_add_iff : Π {x y₁ y₂ : pgame},
+  x ∈ᵣ y₁ + y₂ ↔ (∃ i, x ≡ (y₁.move_right i) + y₂) ∨ (∃ i, x ≡ y₁ + (y₂.move_right i))
+| (mk x₁l x₁r x₁L x₁R) (mk x₂l x₂r x₂L x₂R) (mk yl yr yL yR) := begin
+  constructor,
+  { rintros ⟨(i | i), hi⟩, exacts [or.inl ⟨_, hi⟩, or.inr ⟨_, hi⟩], },
+  { rintros (⟨i, h⟩ | ⟨i, h⟩), exacts [⟨sum.inl i, h⟩, ⟨sum.inr i, h⟩], },
+end
+
+lemma add_comm : Π (x y : pgame.{u}), x + y ≡ y + x
+| (mk xl xr xL xR) (mk yl yr yL yR) := begin
+  refine identical.ext (λ z, _) (λ z, _),
+  { simp_rw [memₗ_add_iff], rw [or.comm], dsimp,
+    simp_rw [(add_comm (xL _) _).congr_right, (add_comm _ (yL _)).congr_right], },
+  { simp_rw [memᵣ_add_iff], rw [or.comm], dsimp,
+    simp_rw [(add_comm (xR _) _).congr_right, (add_comm _ (yR _)).congr_right], },
+end
+using_well_founded { dec_tac := pgame_wf_tac }
+
+lemma exists_left_moves_add {x y : pgame.{u}} {p : (x + y).left_moves → Prop} :
+  (∃ i, p i) ↔
+    (∃ i, p (to_left_moves_add (sum.inl i))) ∨ (∃ i, p (to_left_moves_add (sum.inr i))) :=
+begin
+  cases x with xl xr xL xR; cases y with yl yr yL yR,
+  constructor,
+  { rintros ⟨(i | i), hi⟩, exacts [or.inl ⟨i, hi⟩, or.inr ⟨i, hi⟩], },
+  { rintros (⟨i, hi⟩ | ⟨i, hi⟩), exacts [⟨_, hi⟩, ⟨_, hi⟩], }
+end
+
+lemma exists_right_moves_add {x y : pgame.{u}} {p : (x + y).right_moves → Prop} :
+  (∃ i, p i) ↔
+    (∃ i, p (to_right_moves_add (sum.inl i))) ∨ (∃ i, p (to_right_moves_add (sum.inr i))) :=
+begin
+  cases x with xl xr xL xR; cases y with yl yr yL yR,
+  constructor,
+  { rintros ⟨(i | i), hi⟩, exacts [or.inl ⟨i, hi⟩, or.inr ⟨i, hi⟩], },
+  { rintros (⟨i, hi⟩ | ⟨i, hi⟩), exacts [⟨_, hi⟩, ⟨_, hi⟩], }
+end
+
+lemma add_assoc : Π (x y z : pgame.{u}), x + y + z ≡ x + (y + z)
+| (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR) := begin
+  refine identical.ext (λ z, _) (λ z, _),
+  { simp_rw [memₗ_add_iff, exists_left_moves_add, or.assoc,
+      add_move_left_inl, add_move_left_inr, (add_assoc _ _ _).congr_right], },
+  { simp_rw [memᵣ_add_iff, exists_right_moves_add, or.assoc,
+      add_move_right_inl, add_move_right_inr, (add_assoc _ _ _).congr_right], },
+end
+using_well_founded { dec_tac := pgame_wf_tac }
+
+lemma add_zero : Π (x : pgame), x + 0 ≡ x
+| (mk xl xr xL xR) := begin
+  refine identical.ext (λ z, _) (λ z, _),
+  { simp_rw [memₗ_add_iff, is_empty.exists_iff, or_false, (add_zero _).congr_right], refl },
+  { simp_rw [memᵣ_add_iff, is_empty.exists_iff, or_false, (add_zero _).congr_right], refl },
+end
+using_well_founded { dec_tac := pgame_wf_tac }
+
+lemma zero_add (x : pgame) : 0 + x ≡ x :=
+(add_comm _ _).trans (add_zero _)
+
+lemma neg_add_rev : Π (x y : pgame.{u}), -(x + y) ≡ -y + -x
+| (mk xl xr xL xR) (mk yl yr yL yR) := begin
+  refine identical.ext (λ z, _) (λ z, _),
+  { simp_rw [memₗ_add_iff, memₗ_neg_iff, exists_right_moves_add,
+      add_move_right_inl, add_move_right_inr, (neg_add_rev _ _).congr_right], rw [or.comm], refl, },
+  { simp_rw [memᵣ_add_iff, memᵣ_neg_iff, exists_left_moves_add,
+      add_move_left_inl, add_move_left_inr, (neg_add_rev _ _).congr_right], rw [or.comm], refl, },
+end
+using_well_founded { dec_tac := pgame_wf_tac }
+
+lemma neg_add (x y : pgame.{u}) : -(x + y) ≡ -x + -y :=
+(neg_add_rev _ _).trans (add_comm _ _)
+
+lemma identical_zero_iff : Π (x : pgame.{u}),
+  x ≡ 0 ↔ is_empty x.left_moves ∧ is_empty x.right_moves
+| (mk xl xr xL xR) := begin
+  constructor,
+  { rintros ⟨h₁, h₂⟩,
+    simp_rw [is_empty.forall_iff, and_true, is_empty.exists_iff] at h₁ h₂,
+    exact ⟨⟨h₁⟩, ⟨h₂⟩⟩, },
+  { rintros ⟨h₁, h₂⟩, exactI identical_of_is_empty _ _, },
+end
+
+lemma add_eq_zero_iff : Π (x y : pgame.{u}), x + y ≡ 0 ↔ x ≡ 0 ∧ y ≡ 0
+| (mk xl xr xL xR) (mk yl yr yL yR) :=
+by { simp_rw [identical_zero_iff, left_moves_add, right_moves_add, is_empty_sum], tauto, }
+
+lemma identical.add_right : Π {x₁ x₂ y}, x₁ ≡ x₂ → x₁ + y ≡ x₂ + y
+| (mk x₁l x₁r x₁L x₁R) (mk x₂l x₂r x₂L x₂R) (mk yl yr yL yR) := begin
+  rintros ⟨⟨hL₁, hL₂⟩, ⟨hR₁, hR₂⟩⟩,
+  have h : (mk x₁l x₁r x₁L x₁R) ≡ (mk x₂l x₂r x₂L x₂R) := ⟨⟨hL₁, hL₂⟩, ⟨hR₁, hR₂⟩⟩,
+  refine identical.ext (λ z, _) (λ z, _),
+  { simp_rw [memₗ_add_iff, h.add_right.congr_right],
+    exact or_congr_left' ⟨λ ⟨i, hi⟩, (hL₁ i).imp (λ j hj, hi.trans hj.add_right),
+        λ ⟨i, hi⟩, (hL₂ i).imp (λ j hj, hi.trans hj.add_right.symm)⟩ },
+  { simp_rw [memᵣ_add_iff, h.add_right.congr_right],
+    exact or_congr_left' ⟨λ ⟨i, hi⟩, (hR₁ i).imp (λ j hj, hi.trans hj.add_right),
+        λ ⟨i, hi⟩, (hR₂ i).imp (λ j hj, hi.trans hj.add_right.symm)⟩ },
+end
+using_well_founded { dec_tac := pgame_wf_tac }
+
+lemma identical.add_left {x y₁ y₂} (hy : y₁ ≡ y₂) : x + y₁ ≡ x + y₂ :=
+(add_comm _ _).trans (hy.add_right.trans (add_comm _ _))
+
+lemma identical.add {x₁ x₂ y₁ y₂ : pgame.{u}} (hx : x₁ ≡ x₂) (hy : y₁ ≡ y₂) : x₁ + y₁ ≡ x₂ + y₂ :=
+hx.add_right.trans hy.add_left
+
+lemma memₗ_add_iff' : Π {x y₁ y₂ : pgame},
+  x ∈ₗ y₁ + y₂ ↔ (∃ z ∈ₗ y₁, x ≡ z + y₂) ∨ (∃ z ∈ₗ y₂, x ≡ y₁ + z)
+| (mk x₁l x₁r x₁L x₁R) (mk x₂l x₂r x₂L x₂R) (mk yl yr yL yR) := memₗ_add_iff.trans $ or_congr
+  ⟨λ ⟨i, hi⟩, ⟨_, ⟨_, refl _⟩, hi⟩, λ ⟨_, ⟨i, hi⟩, h⟩, ⟨i, h.trans hi.add_right⟩⟩
+  ⟨λ ⟨i, hi⟩, ⟨_, ⟨_, refl _⟩, hi⟩, λ ⟨_, ⟨i, hi⟩, h⟩, ⟨i, h.trans hi.add_left⟩⟩
+
+lemma memᵣ_add_iff' : Π {x y₁ y₂ : pgame},
+  x ∈ᵣ y₁ + y₂ ↔ (∃ z ∈ᵣ y₁, x ≡ z + y₂) ∨ (∃ z ∈ᵣ y₂, x ≡ y₁ + z)
+| (mk x₁l x₁r x₁L x₁R) (mk x₂l x₂r x₂L x₂R) (mk yl yr yL yR) := memᵣ_add_iff.trans $ or_congr
+  ⟨λ ⟨i, hi⟩, ⟨_, ⟨_, refl _⟩, hi⟩, λ ⟨_, ⟨i, hi⟩, h⟩, ⟨i, h.trans hi.add_right⟩⟩
+  ⟨λ ⟨i, hi⟩, ⟨_, ⟨_, refl _⟩, hi⟩, λ ⟨_, ⟨i, hi⟩, h⟩, ⟨i, h.trans hi.add_left⟩⟩
+
 /-- If `w` has the same moves as `x` and `y` has the same moves as `z`,
 then `w + y` has the same moves as `x + z`. -/
 def relabelling.add_congr : ∀ {w x y z : pgame.{u}}, w ≡r x → y ≡r z → w + y ≡r x + z

From 1b3d193b22d710f9c88649fa8df080f32ed22b0d Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 1 Mar 2023 02:40:50 +0800
Subject: [PATCH 02/22] docs, protected

---
 src/set_theory/game/pgame.lean | 26 +++++++++++++++++---------
 1 file changed, 17 insertions(+), 9 deletions(-)

diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index 39fc90293e68c..15783656f6230 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -710,6 +710,11 @@ end forall_exists_rel
 namespace pgame
 open_locale pgame
 
+/-! ### Identity -/
+
+/-- Two pre-games are identical if their left and right sets are identical.
+That is, `identical x y` if every left move of `x` is identical to some left move of `y`,
+every right move of `x` is identical to some right move of `y`, and vice versa. -/
 def identical : Π (x y : pgame), Prop
 | (mk _ _ xL xR) (mk _ _ yL yR) :=
   ((∀ i, ∃ j, identical (xL i) (yL j)) ∧ (∀ j, ∃ i, identical (xL i) (yL j))) ∧
@@ -717,7 +722,10 @@ def identical : Π (x y : pgame), Prop
 
 localized "infix (name := pgame.identical) ` ≡ `:50 := pgame.identical" in pgame
 
+/-- `x ∈ₗ y` if `x` is identical to some left move of `y`. -/
 def memₗ (x y : pgame.{u}) : Prop := ∃ b, x ≡ (y.move_left b)
+
+/-- `x ∈ᵣ y` if `x` is identical to some right move of `y`. -/
 def memᵣ (x y : pgame.{u}) : Prop := ∃ b, x ≡ (y.move_right b)
 
 localized "infix (name := pgame.memₗ) ` ∈ₗ `:50 := pgame.memₗ" in pgame
@@ -1304,7 +1312,7 @@ lemma memᵣ_add_iff : Π {x y₁ y₂ : pgame},
   { rintros (⟨i, h⟩ | ⟨i, h⟩), exacts [⟨sum.inl i, h⟩, ⟨sum.inr i, h⟩], },
 end
 
-lemma add_comm : Π (x y : pgame.{u}), x + y ≡ y + x
+protected lemma add_comm : Π (x y : pgame.{u}), x + y ≡ y + x
 | (mk xl xr xL xR) (mk yl yr yL yR) := begin
   refine identical.ext (λ z, _) (λ z, _),
   { simp_rw [memₗ_add_iff], rw [or.comm], dsimp,
@@ -1334,7 +1342,7 @@ begin
   { rintros (⟨i, hi⟩ | ⟨i, hi⟩), exacts [⟨_, hi⟩, ⟨_, hi⟩], }
 end
 
-lemma add_assoc : Π (x y z : pgame.{u}), x + y + z ≡ x + (y + z)
+protected lemma add_assoc : Π (x y z : pgame.{u}), x + y + z ≡ x + (y + z)
 | (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR) := begin
   refine identical.ext (λ z, _) (λ z, _),
   { simp_rw [memₗ_add_iff, exists_left_moves_add, or.assoc,
@@ -1344,7 +1352,7 @@ lemma add_assoc : Π (x y z : pgame.{u}), x + y + z ≡ x + (y + z)
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
-lemma add_zero : Π (x : pgame), x + 0 ≡ x
+protected lemma add_zero : Π (x : pgame), x + 0 ≡ x
 | (mk xl xr xL xR) := begin
   refine identical.ext (λ z, _) (λ z, _),
   { simp_rw [memₗ_add_iff, is_empty.exists_iff, or_false, (add_zero _).congr_right], refl },
@@ -1352,10 +1360,10 @@ lemma add_zero : Π (x : pgame), x + 0 ≡ x
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
-lemma zero_add (x : pgame) : 0 + x ≡ x :=
-(add_comm _ _).trans (add_zero _)
+protected lemma zero_add (x : pgame) : 0 + x ≡ x :=
+(pgame.add_comm _ _).trans x.add_zero
 
-lemma neg_add_rev : Π (x y : pgame.{u}), -(x + y) ≡ -y + -x
+protected lemma neg_add_rev : Π (x y : pgame.{u}), -(x + y) ≡ -y + -x
 | (mk xl xr xL xR) (mk yl yr yL yR) := begin
   refine identical.ext (λ z, _) (λ z, _),
   { simp_rw [memₗ_add_iff, memₗ_neg_iff, exists_right_moves_add,
@@ -1365,8 +1373,8 @@ lemma neg_add_rev : Π (x y : pgame.{u}), -(x + y) ≡ -y + -x
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
-lemma neg_add (x y : pgame.{u}) : -(x + y) ≡ -x + -y :=
-(neg_add_rev _ _).trans (add_comm _ _)
+protected lemma neg_add (x y : pgame.{u}) : -(x + y) ≡ -x + -y :=
+(x.neg_add_rev y).trans (pgame.add_comm _ _)
 
 lemma identical_zero_iff : Π (x : pgame.{u}),
   x ≡ 0 ↔ is_empty x.left_moves ∧ is_empty x.right_moves
@@ -1397,7 +1405,7 @@ end
 using_well_founded { dec_tac := pgame_wf_tac }
 
 lemma identical.add_left {x y₁ y₂} (hy : y₁ ≡ y₂) : x + y₁ ≡ x + y₂ :=
-(add_comm _ _).trans (hy.add_right.trans (add_comm _ _))
+(x.add_comm y₁).trans (hy.add_right.trans (y₂.add_comm x))
 
 lemma identical.add {x₁ x₂ y₁ y₂ : pgame.{u}} (hx : x₁ ≡ x₂) (hy : y₁ ≡ y₂) : x₁ + y₁ ≡ x₂ + y₂ :=
 hx.add_right.trans hy.add_left

From fe3964700ff0920072f58445b0aba801ba9f6aa9 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 1 Mar 2023 03:14:04 +0800
Subject: [PATCH 03/22] mem mul

---
 src/set_theory/game/basic.lean | 20 ++++++++++++++++++++
 src/set_theory/game/pgame.lean |  4 ++--
 2 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/src/set_theory/game/basic.lean b/src/set_theory/game/basic.lean
index c440ab66e49f4..a4cafd4ed4e08 100644
--- a/src/set_theory/game/basic.lean
+++ b/src/set_theory/game/basic.lean
@@ -263,6 +263,26 @@ begin
   { apply hr }
 end
 
+lemma memₗ_mul_iff : Π {x y₁ y₂ : pgame},
+  x ∈ₗ y₁ * y₂ ↔
+    (∃ i j, x ≡ y₁.move_left i * y₂ + y₁ * y₂.move_left j - y₁.move_left i * y₂.move_left j) ∨
+    (∃ i j, x ≡ y₁.move_right i * y₂ + y₁ * y₂.move_right j - y₁.move_right i * y₂.move_right j)
+| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := begin
+  constructor,
+  { rintros ⟨(⟨i, j⟩ | ⟨i, j⟩), hi⟩, exacts [or.inl ⟨_, _, hi⟩, or.inr ⟨_, _, hi⟩], },
+  { rintros (⟨i, j, h⟩ | ⟨i, j, h⟩), exacts [⟨sum.inl (i, j), h⟩, ⟨sum.inr (i, j), h⟩], },
+end
+
+lemma memᵣ_mul_iff : Π {x y₁ y₂ : pgame},
+  x ∈ᵣ y₁ * y₂ ↔
+    (∃ i j, x ≡ y₁.move_left i * y₂ + y₁ * y₂.move_right j - y₁.move_left i * y₂.move_right j) ∨
+    (∃ i j, x ≡ y₁.move_right i * y₂ + y₁ * y₂.move_left j - y₁.move_right i * y₂.move_left j)
+| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := begin
+  constructor,
+  { rintros ⟨(⟨i, j⟩ | ⟨i, j⟩), hi⟩, exacts [or.inl ⟨_, _, hi⟩, or.inr ⟨_, _, hi⟩], },
+  { rintros (⟨i, j, h⟩ | ⟨i, j, h⟩), exacts [⟨sum.inl (i, j), h⟩, ⟨sum.inr (i, j), h⟩], },
+end
+
 /-- `x * y` and `y * x` have the same moves. -/
 def mul_comm_relabelling : Π (x y : pgame.{u}), x * y ≡r y * x
 | ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ := begin
diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index 15783656f6230..235d6e3c4a83a 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -1298,7 +1298,7 @@ end
 
 lemma memₗ_add_iff : Π {x y₁ y₂ : pgame},
   x ∈ₗ y₁ + y₂ ↔ (∃ i, x ≡ (y₁.move_left i) + y₂) ∨ (∃ i, x ≡ y₁ + (y₂.move_left i))
-| (mk x₁l x₁r x₁L x₁R) (mk x₂l x₂r x₂L x₂R) (mk yl yr yL yR) := begin
+| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := begin
   constructor,
   { rintros ⟨(i | i), hi⟩, exacts [or.inl ⟨_, hi⟩, or.inr ⟨_, hi⟩], },
   { rintros (⟨i, h⟩ | ⟨i, h⟩), exacts [⟨sum.inl i, h⟩, ⟨sum.inr i, h⟩], },
@@ -1306,7 +1306,7 @@ end
 
 lemma memᵣ_add_iff : Π {x y₁ y₂ : pgame},
   x ∈ᵣ y₁ + y₂ ↔ (∃ i, x ≡ (y₁.move_right i) + y₂) ∨ (∃ i, x ≡ y₁ + (y₂.move_right i))
-| (mk x₁l x₁r x₁L x₁R) (mk x₂l x₂r x₂L x₂R) (mk yl yr yL yR) := begin
+| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := begin
   constructor,
   { rintros ⟨(i | i), hi⟩, exacts [or.inl ⟨_, hi⟩, or.inr ⟨_, hi⟩], },
   { rintros (⟨i, h⟩ | ⟨i, h⟩), exacts [⟨sum.inl i, h⟩, ⟨sum.inr i, h⟩], },

From 415aea22c5de20922286320484aba909503aae48 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 1 Mar 2023 03:35:32 +0800
Subject: [PATCH 04/22] mul_comm

---
 src/set_theory/game/basic.lean | 19 ++++++++++++++++++-
 src/set_theory/game/pgame.lean |  4 ++--
 2 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/src/set_theory/game/basic.lean b/src/set_theory/game/basic.lean
index a4cafd4ed4e08..c4cfc18db1024 100644
--- a/src/set_theory/game/basic.lean
+++ b/src/set_theory/game/basic.lean
@@ -146,7 +146,7 @@ but to prove their properties we need to use the abelian group structure of game
 Hence we define them here. -/
 
 /-- The product of `x = {xL | xR}` and `y = {yL | yR}` is
-`{xL*y + x*yL - xL*yL, xR*y + x*yR - xR*yR | xL*y + x*yR - xL*yR, x*yL + xR*y - xR*yL }`. -/
+`{xL*y + x*yL - xL*yL, xR*y + x*yR - xR*yR | xL*y + x*yR - xL*yR, xR*y + x*yL - xR*yL }`. -/
 instance : has_mul pgame.{u} :=
 ⟨λ x y, begin
   induction x with xl xr xL xR IHxl IHxr generalizing y,
@@ -283,6 +283,23 @@ lemma memᵣ_mul_iff : Π {x y₁ y₂ : pgame},
   { rintros (⟨i, j, h⟩ | ⟨i, j, h⟩), exacts [⟨sum.inl (i, j), h⟩, ⟨sum.inr (i, j), h⟩], },
 end
 
+/-- `x * y` and `y * x` have the same moves. -/
+protected def mul_comm : Π (x y : pgame.{u}), x * y ≡ y * x
+| ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ := begin
+  refine identical.ext (λ z, _) (λ z, _),
+  { simp_rw [memₗ_mul_iff], dsimp, rw [@exists_comm xl, @exists_comm xr],
+    simp_rw [((((mul_comm _ _).add (mul_comm _ _)).trans ((_ * xL _).add_comm _)).sub
+        (mul_comm _ _)).congr_right,
+      ((((mul_comm _ _).add (mul_comm _ _)).trans ((_ * xR _).add_comm _)).sub
+        (mul_comm _ _)).congr_right], },
+  { simp_rw [memᵣ_mul_iff], dsimp, rw [@exists_comm xl, @exists_comm xr, or.comm],
+    simp_rw [((((mul_comm _ _).add (mul_comm _ _)).trans ((_ * xL _).add_comm _)).sub
+        (mul_comm _ _)).congr_right,
+      ((((mul_comm _ _).add (mul_comm _ _)).trans ((_ * xR _).add_comm _)).sub
+        (mul_comm _ _)).congr_right], },
+end
+using_well_founded { dec_tac := pgame_wf_tac }
+
 /-- `x * y` and `y * x` have the same moves. -/
 def mul_comm_relabelling : Π (x y : pgame.{u}), x * y ≡r y * x
 | ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ := begin
diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index 235d6e3c4a83a..dd10a2034de59 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -1315,9 +1315,9 @@ end
 protected lemma add_comm : Π (x y : pgame.{u}), x + y ≡ y + x
 | (mk xl xr xL xR) (mk yl yr yL yR) := begin
   refine identical.ext (λ z, _) (λ z, _),
-  { simp_rw [memₗ_add_iff], rw [or.comm], dsimp,
+  { simp_rw [memₗ_add_iff], dsimp, rw [or.comm],
     simp_rw [(add_comm (xL _) _).congr_right, (add_comm _ (yL _)).congr_right], },
-  { simp_rw [memᵣ_add_iff], rw [or.comm], dsimp,
+  { simp_rw [memᵣ_add_iff], dsimp, rw [or.comm],
     simp_rw [(add_comm (xR _) _).congr_right, (add_comm _ (yR _)).congr_right], },
 end
 using_well_founded { dec_tac := pgame_wf_tac }

From d2e5ec35eeb64a4614ab55590312a7515abdd71b Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 1 Mar 2023 03:51:57 +0800
Subject: [PATCH 05/22] `identical_zero` `identical.sub`

---
 src/set_theory/game/pgame.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index dd10a2034de59..0b4921c2a2b00 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -1386,6 +1386,10 @@ lemma identical_zero_iff : Π (x : pgame.{u}),
   { rintros ⟨h₁, h₂⟩, exactI identical_of_is_empty _ _, },
 end
 
+/-- Any game without left or right moves is identival to 0. -/
+def identical_zero (x : pgame) [is_empty x.left_moves] [is_empty x.right_moves] : x ≡ 0 :=
+x.identical_zero_iff.mpr ⟨by apply_instance, by apply_instance⟩
+
 lemma add_eq_zero_iff : Π (x y : pgame.{u}), x + y ≡ 0 ↔ x ≡ 0 ∧ y ≡ 0
 | (mk xl xr xL xR) (mk yl yr yL yR) :=
 by { simp_rw [identical_zero_iff, left_moves_add, right_moves_add, is_empty_sum], tauto, }
@@ -1444,6 +1448,9 @@ instance : has_sub pgame := ⟨λ x y, x + -y⟩
 @[simp] theorem sub_zero (x : pgame) : x - 0 = x + 0 :=
 show x + -0 = x + 0, by rw neg_zero
 
+lemma identical.sub {x₁ x₂ y₁ y₂ : pgame.{u}} (hx : x₁ ≡ x₂) (hy : y₁ ≡ y₂) : x₁ - y₁ ≡ x₂ - y₂ :=
+hx.add hy.neg
+
 /-- If `w` has the same moves as `x` and `y` has the same moves as `z`,
 then `w - y` has the same moves as `x - z`. -/
 def relabelling.sub_congr {w x y z : pgame} (h₁ : w ≡r x) (h₂ : y ≡r z) : w - y ≡r x - z :=

From f61ce93f640cf5c178dc9cfe77cd8caf73b3a3e9 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 1 Mar 2023 04:07:02 +0800
Subject: [PATCH 06/22] golf

---
 src/set_theory/game/pgame.lean | 44 ++++++++++++++--------------------
 1 file changed, 18 insertions(+), 26 deletions(-)

diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index 0b4921c2a2b00..82cbc8287bf23 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -1296,32 +1296,6 @@ instance is_empty_nat_right_moves : ∀ n : ℕ, is_empty (right_moves n)
   apply_instance
 end
 
-lemma memₗ_add_iff : Π {x y₁ y₂ : pgame},
-  x ∈ₗ y₁ + y₂ ↔ (∃ i, x ≡ (y₁.move_left i) + y₂) ∨ (∃ i, x ≡ y₁ + (y₂.move_left i))
-| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := begin
-  constructor,
-  { rintros ⟨(i | i), hi⟩, exacts [or.inl ⟨_, hi⟩, or.inr ⟨_, hi⟩], },
-  { rintros (⟨i, h⟩ | ⟨i, h⟩), exacts [⟨sum.inl i, h⟩, ⟨sum.inr i, h⟩], },
-end
-
-lemma memᵣ_add_iff : Π {x y₁ y₂ : pgame},
-  x ∈ᵣ y₁ + y₂ ↔ (∃ i, x ≡ (y₁.move_right i) + y₂) ∨ (∃ i, x ≡ y₁ + (y₂.move_right i))
-| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := begin
-  constructor,
-  { rintros ⟨(i | i), hi⟩, exacts [or.inl ⟨_, hi⟩, or.inr ⟨_, hi⟩], },
-  { rintros (⟨i, h⟩ | ⟨i, h⟩), exacts [⟨sum.inl i, h⟩, ⟨sum.inr i, h⟩], },
-end
-
-protected lemma add_comm : Π (x y : pgame.{u}), x + y ≡ y + x
-| (mk xl xr xL xR) (mk yl yr yL yR) := begin
-  refine identical.ext (λ z, _) (λ z, _),
-  { simp_rw [memₗ_add_iff], dsimp, rw [or.comm],
-    simp_rw [(add_comm (xL _) _).congr_right, (add_comm _ (yL _)).congr_right], },
-  { simp_rw [memᵣ_add_iff], dsimp, rw [or.comm],
-    simp_rw [(add_comm (xR _) _).congr_right, (add_comm _ (yR _)).congr_right], },
-end
-using_well_founded { dec_tac := pgame_wf_tac }
-
 lemma exists_left_moves_add {x y : pgame.{u}} {p : (x + y).left_moves → Prop} :
   (∃ i, p i) ↔
     (∃ i, p (to_left_moves_add (sum.inl i))) ∨ (∃ i, p (to_left_moves_add (sum.inr i))) :=
@@ -1342,6 +1316,24 @@ begin
   { rintros (⟨i, hi⟩ | ⟨i, hi⟩), exacts [⟨_, hi⟩, ⟨_, hi⟩], }
 end
 
+lemma memₗ_add_iff : Π {x y₁ y₂ : pgame},
+  x ∈ₗ y₁ + y₂ ↔ (∃ i, x ≡ (y₁.move_left i) + y₂) ∨ (∃ i, x ≡ y₁ + (y₂.move_left i))
+| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := exists_left_moves_add
+
+lemma memᵣ_add_iff : Π {x y₁ y₂ : pgame},
+  x ∈ᵣ y₁ + y₂ ↔ (∃ i, x ≡ (y₁.move_right i) + y₂) ∨ (∃ i, x ≡ y₁ + (y₂.move_right i))
+| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := exists_right_moves_add
+
+protected lemma add_comm : Π (x y : pgame.{u}), x + y ≡ y + x
+| (mk xl xr xL xR) (mk yl yr yL yR) := begin
+  refine identical.ext (λ z, _) (λ z, _),
+  { simp_rw [memₗ_add_iff], dsimp, rw [or.comm],
+    simp_rw [(add_comm (xL _) _).congr_right, (add_comm _ (yL _)).congr_right], },
+  { simp_rw [memᵣ_add_iff], dsimp, rw [or.comm],
+    simp_rw [(add_comm (xR _) _).congr_right, (add_comm _ (yR _)).congr_right], },
+end
+using_well_founded { dec_tac := pgame_wf_tac }
+
 protected lemma add_assoc : Π (x y z : pgame.{u}), x + y + z ≡ x + (y + z)
 | (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR) := begin
   refine identical.ext (λ z, _) (λ z, _),

From 371fefb349b91f7420528fe12eb1d61e07c38650 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 1 Mar 2023 06:02:14 +0800
Subject: [PATCH 07/22] more lemmas

---
 src/set_theory/game/basic.lean | 89 +++++++++++++++++++++++++++++-----
 src/set_theory/game/pgame.lean | 46 ++++++++++++++----
 2 files changed, 115 insertions(+), 20 deletions(-)

diff --git a/src/set_theory/game/basic.lean b/src/set_theory/game/basic.lean
index c4cfc18db1024..ac584251bbe5d 100644
--- a/src/set_theory/game/basic.lean
+++ b/src/set_theory/game/basic.lean
@@ -263,28 +263,42 @@ begin
   { apply hr }
 end
 
+lemma exists_left_moves_mul {x y : pgame.{u}} {p : (x * y).left_moves → Prop} :
+  (∃ i, p i) ↔
+    (∃ i j, p (to_left_moves_mul (sum.inl (i, j)))) ∨
+    (∃ i j, p (to_left_moves_mul (sum.inr (i, j)))) :=
+begin
+  cases x with xl xr xL xR; cases y with yl yr yL yR,
+  constructor,
+  { rintros ⟨(⟨i, j⟩ | ⟨i, j⟩), hi⟩, exacts [or.inl ⟨i, j, hi⟩, or.inr ⟨i, j, hi⟩], },
+  { rintros (⟨i, j, h⟩ | ⟨i, j, h⟩), exacts [⟨_, h⟩, ⟨_, h⟩], },
+end
+
+lemma exists_right_moves_mul {x y : pgame.{u}} {p : (x * y).right_moves → Prop} :
+  (∃ i, p i) ↔
+    (∃ i j, p (to_right_moves_mul (sum.inl (i, j)))) ∨
+    (∃ i j, p (to_right_moves_mul (sum.inr (i, j)))) :=
+begin
+  cases x with xl xr xL xR; cases y with yl yr yL yR,
+  constructor,
+  { rintros ⟨(⟨i, j⟩ | ⟨i, j⟩), hi⟩, exacts [or.inl ⟨i, j, hi⟩, or.inr ⟨i, j, hi⟩], },
+  { rintros (⟨i, j, h⟩ | ⟨i, j, h⟩), exacts [⟨_, h⟩, ⟨_, h⟩], },
+end
+
 lemma memₗ_mul_iff : Π {x y₁ y₂ : pgame},
   x ∈ₗ y₁ * y₂ ↔
     (∃ i j, x ≡ y₁.move_left i * y₂ + y₁ * y₂.move_left j - y₁.move_left i * y₂.move_left j) ∨
     (∃ i j, x ≡ y₁.move_right i * y₂ + y₁ * y₂.move_right j - y₁.move_right i * y₂.move_right j)
-| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := begin
-  constructor,
-  { rintros ⟨(⟨i, j⟩ | ⟨i, j⟩), hi⟩, exacts [or.inl ⟨_, _, hi⟩, or.inr ⟨_, _, hi⟩], },
-  { rintros (⟨i, j, h⟩ | ⟨i, j, h⟩), exacts [⟨sum.inl (i, j), h⟩, ⟨sum.inr (i, j), h⟩], },
-end
+| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := exists_left_moves_mul
 
 lemma memᵣ_mul_iff : Π {x y₁ y₂ : pgame},
   x ∈ᵣ y₁ * y₂ ↔
     (∃ i j, x ≡ y₁.move_left i * y₂ + y₁ * y₂.move_right j - y₁.move_left i * y₂.move_right j) ∨
     (∃ i j, x ≡ y₁.move_right i * y₂ + y₁ * y₂.move_left j - y₁.move_right i * y₂.move_left j)
-| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := begin
-  constructor,
-  { rintros ⟨(⟨i, j⟩ | ⟨i, j⟩), hi⟩, exacts [or.inl ⟨_, _, hi⟩, or.inr ⟨_, _, hi⟩], },
-  { rintros (⟨i, j, h⟩ | ⟨i, j, h⟩), exacts [⟨sum.inl (i, j), h⟩, ⟨sum.inr (i, j), h⟩], },
-end
+| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := exists_right_moves_mul
 
 /-- `x * y` and `y * x` have the same moves. -/
-protected def mul_comm : Π (x y : pgame.{u}), x * y ≡ y * x
+protected lemma mul_comm : Π (x y : pgame.{u}), x * y ≡ y * x
 | ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ := begin
   refine identical.ext (λ z, _) (λ z, _),
   { simp_rw [memₗ_mul_iff], dsimp, rw [@exists_comm xl, @exists_comm xr],
@@ -328,6 +342,9 @@ by { cases x, apply sum.is_empty }
 instance is_empty_zero_mul_right_moves (x : pgame.{u}) : is_empty (0 * x).right_moves :=
 by { cases x, apply sum.is_empty }
 
+/-- `x * 0` has exactly the same moves as `0`. -/
+protected def mul_zero (x : pgame) : x * 0 ≡ 0 := identical_zero _
+
 /-- `x * 0` has exactly the same moves as `0`. -/
 def mul_zero_relabelling (x : pgame) : x * 0 ≡r 0 := relabelling.is_empty _
 
@@ -337,6 +354,9 @@ theorem mul_zero_equiv (x : pgame) : x * 0 ≈ 0 := (mul_zero_relabelling x).equ
 @[simp] theorem quot_mul_zero (x : pgame) : ⟦x * 0⟧ = ⟦0⟧ :=
 @quotient.sound _ _ (x * 0) _ x.mul_zero_equiv
 
+/-- `0 * x` has exactly the same moves as `0`. -/
+protected def zero_mul (x : pgame) : 0 * x ≡ 0 := identical_zero _
+
 /-- `0 * x` has exactly the same moves as `0`. -/
 def zero_mul_relabelling (x : pgame) : 0 * x ≡r 0 := relabelling.is_empty _
 
@@ -358,6 +378,39 @@ def neg_mul_relabelling : Π (x y : pgame.{u}), -x * y ≡r -(x * y)
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
+/-- `x * -y` and `-(x * y)` have the same moves. -/
+lemma mul_neg : Π (x y : pgame.{u}), x * -y = -(x * y)
+| (mk xl xr xL xR) (mk yl yr yL yR) := begin
+  refine ext rfl rfl _ _,
+  { rintros (⟨i, j⟩ | ⟨i, j⟩) _ ⟨rfl⟩,
+    { refine (@mul_move_left_inl (mk xl xr xL xR) (-mk yl yr yL yR) i j).trans _,
+      dsimp [to_left_moves_neg],
+      rw [pgame.neg_sub', pgame.neg_add],
+      congr',
+      exacts [mul_neg _ (mk _ _ _ _), mul_neg _ _, mul_neg _ _], },
+    { refine (@mul_move_left_inr (mk xl xr xL xR) (-mk yl yr yL yR) i j).trans _,
+      dsimp [to_left_moves_neg],
+      rw [pgame.neg_sub', pgame.neg_add],
+      congr',
+      exacts [mul_neg _ (mk _ _ _ _), mul_neg _ _, mul_neg _ _], }, },
+  { rintros (⟨i, j⟩ | ⟨i, j⟩) _ ⟨rfl⟩,
+    { refine (@mul_move_right_inl (mk xl xr xL xR) (-mk yl yr yL yR) i j).trans _,
+      dsimp [to_left_moves_neg],
+      rw [pgame.neg_sub', pgame.neg_add],
+      congr',
+      exacts [mul_neg _ (mk _ _ _ _), mul_neg _ _, mul_neg _ _], },
+    { refine (@mul_move_right_inr (mk xl xr xL xR) (-mk yl yr yL yR) i j).trans _,
+      dsimp [to_left_moves_neg],
+      rw [pgame.neg_sub', pgame.neg_add],
+      congr',
+      exacts [mul_neg _ (mk _ _ _ _), mul_neg _ _, mul_neg _ _], }, },
+end
+using_well_founded { dec_tac := pgame_wf_tac }
+
+/-- `-x * y` and `-(x * y)` have the same moves. -/
+def neg_mul (x y : pgame.{u}) : -x * y ≡ -(x * y) :=
+((pgame.mul_comm _ _).trans (of_eq (mul_neg _ _))).trans (pgame.mul_comm _ _).neg
+
 @[simp] theorem quot_neg_mul (x y : pgame) : ⟦-x * y⟧ = -⟦x * y⟧ :=
 quot.sound (neg_mul_relabelling x y).equiv
 
@@ -450,6 +503,20 @@ def mul_one_relabelling : Π (x : pgame.{u}), x * 1 ≡r x
     (mul_zero_relabelling _)).trans $ add_zero_relabelling _)
 end
 
+/-- `x * 1` has the same moves as `x`. -/
+def mul_one : Π (x : pgame.{u}), x * 1 ≡ x
+| ⟨xl, xr, xL, xR⟩ := begin
+  unfold has_one.one,
+  refine ⟨(equiv.sum_empty _ _).trans (equiv.prod_punit _),
+    (equiv.empty_sum _ _).trans (equiv.prod_punit _), _, _⟩;
+  try { rintro (⟨i, ⟨ ⟩⟩ | ⟨i, ⟨ ⟩⟩) }; try { intro i };
+  dsimp;
+  apply (relabelling.sub_congr (relabelling.refl _) (mul_zero_relabelling _)).trans;
+  rw sub_zero;
+  exact (add_zero_relabelling _).trans (((mul_one_relabelling _).add_congr
+    (mul_zero_relabelling _)).trans $ add_zero_relabelling _)
+end
+
 @[simp] theorem quot_mul_one (x : pgame) : ⟦x * 1⟧ = ⟦x⟧ := quot.sound $ mul_one_relabelling x
 
 /-- `x * 1` is equivalent to `x`. -/
diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index 82cbc8287bf23..d78c9fe2f301a 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -129,6 +129,18 @@ def move_right : Π (g : pgame), right_moves g → pgame
 @[simp] lemma right_moves_mk {xl xr xL xR} : (⟨xl, xr, xL, xR⟩ : pgame).right_moves = xr := rfl
 @[simp] lemma move_right_mk {xl xr xL xR} : (⟨xl, xr, xL, xR⟩ : pgame).move_right = xR := rfl
 
+lemma ext' {x y : pgame.{u}} (hl : x.left_moves = y.left_moves) (hr : x.right_moves = y.right_moves)
+  (hL : x.move_left == y.move_left) (hR : x.move_right == y.move_right) :
+  x = y :=
+by { cases x, cases y, cases hl, cases hr, cases hL, cases hR, refl, }
+
+lemma ext {x y : pgame.{u}} (hl : x.left_moves = y.left_moves) (hr : x.right_moves = y.right_moves)
+  (hL : ∀ i j, i == j → x.move_left i = y.move_left j)
+  (hR : ∀ i j, i == j → x.move_right i = y.move_right j) :
+  x = y :=
+ext' hl hr (function.hfunext hl (λ i j h, heq_of_eq (hL i j h)))
+  (function.hfunext hr (λ i j h, heq_of_eq (hR i j h)))
+
 /--
 Construct a pre-game from list of pre-games describing the available moves for Left and Right.
 -/
@@ -1052,6 +1064,7 @@ lemma memᵣ_neg_iff : Π {x y : pgame},
   x ∈ᵣ -y ↔ (∃ i, x ≡ -(y.move_left i))
 | (mk xl xr xL xR) (mk yl yr yL yR) := iff.rfl
 
+/-- If `x` has the same moves as `y`, then `-x` has the sames moves as `-y`. -/
 lemma identical.neg : Π {x₁ x₂ : pgame.{u}} (hx : x₁ ≡ x₂), -x₁ ≡ -x₂
 | (mk x₁l x₁r x₁L x₁R) (mk x₂l x₂r x₂L x₂R) ⟨⟨hL₁, hL₂⟩, ⟨hR₁, hR₂⟩⟩ :=
   ⟨⟨λ i, (hR₁ i).imp (λ j, identical.neg), λ j, (hR₂ j).imp (λ i, identical.neg)⟩,
@@ -1324,6 +1337,7 @@ lemma memᵣ_add_iff : Π {x y₁ y₂ : pgame},
   x ∈ᵣ y₁ + y₂ ↔ (∃ i, x ≡ (y₁.move_right i) + y₂) ∨ (∃ i, x ≡ y₁ + (y₂.move_right i))
 | (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := exists_right_moves_add
 
+/-- `x + y` has exactly the same moves as `y + x`. -/
 protected lemma add_comm : Π (x y : pgame.{u}), x + y ≡ y + x
 | (mk xl xr xL xR) (mk yl yr yL yR) := begin
   refine identical.ext (λ z, _) (λ z, _),
@@ -1334,6 +1348,7 @@ protected lemma add_comm : Π (x y : pgame.{u}), x + y ≡ y + x
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
+/-- `(x + y) + z` has exactly the same moves as `x + (y + z)`. -/
 protected lemma add_assoc : Π (x y z : pgame.{u}), x + y + z ≡ x + (y + z)
 | (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR) := begin
   refine identical.ext (λ z, _) (λ z, _),
@@ -1344,6 +1359,7 @@ protected lemma add_assoc : Π (x y z : pgame.{u}), x + y + z ≡ x + (y + z)
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
+/-- `x + 0` has exactly the same moves as `x`. -/
 protected lemma add_zero : Π (x : pgame), x + 0 ≡ x
 | (mk xl xr xL xR) := begin
   refine identical.ext (λ z, _) (λ z, _),
@@ -1352,21 +1368,26 @@ protected lemma add_zero : Π (x : pgame), x + 0 ≡ x
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
+/-- `0 + x` has exactly the same moves as `x`. -/
 protected lemma zero_add (x : pgame) : 0 + x ≡ x :=
 (pgame.add_comm _ _).trans x.add_zero
 
-protected lemma neg_add_rev : Π (x y : pgame.{u}), -(x + y) ≡ -y + -x
+/-- `-(x + y)` has exactly the same moves as `-x + -y`. -/
+lemma neg_add : Π (x y : pgame.{u}), -(x + y) = -x + -y
 | (mk xl xr xL xR) (mk yl yr yL yR) := begin
-  refine identical.ext (λ z, _) (λ z, _),
-  { simp_rw [memₗ_add_iff, memₗ_neg_iff, exists_right_moves_add,
-      add_move_right_inl, add_move_right_inr, (neg_add_rev _ _).congr_right], rw [or.comm], refl, },
-  { simp_rw [memᵣ_add_iff, memᵣ_neg_iff, exists_left_moves_add,
-      add_move_left_inl, add_move_left_inr, (neg_add_rev _ _).congr_right], rw [or.comm], refl, },
+  refine ext rfl rfl _ _,
+  { rintros (i | i) _ ⟨rfl⟩,
+    { exact neg_add _ _, },
+    { simpa [to_left_moves_neg] using neg_add _ _, }, },
+  { rintros (i | i) _ ⟨rfl⟩,
+    { exact neg_add _ _, },
+    { simpa [to_right_moves_neg] using neg_add _ _, }, },
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
-protected lemma neg_add (x y : pgame.{u}) : -(x + y) ≡ -x + -y :=
-(x.neg_add_rev y).trans (pgame.add_comm _ _)
+/-- `-(x + y)` has exactly the same moves as `-y + -x`. -/
+protected lemma neg_add_rev (x y : pgame.{u}) : -(x + y) ≡ -y + -x :=
+identical.trans (of_eq (x.neg_add y)) (pgame.add_comm _ _)
 
 lemma identical_zero_iff : Π (x : pgame.{u}),
   x ≡ 0 ↔ is_empty x.left_moves ∧ is_empty x.right_moves
@@ -1379,7 +1400,7 @@ lemma identical_zero_iff : Π (x : pgame.{u}),
 end
 
 /-- Any game without left or right moves is identival to 0. -/
-def identical_zero (x : pgame) [is_empty x.left_moves] [is_empty x.right_moves] : x ≡ 0 :=
+lemma identical_zero (x : pgame) [is_empty x.left_moves] [is_empty x.right_moves] : x ≡ 0 :=
 x.identical_zero_iff.mpr ⟨by apply_instance, by apply_instance⟩
 
 lemma add_eq_zero_iff : Π (x y : pgame.{u}), x + y ≡ 0 ↔ x ≡ 0 ∧ y ≡ 0
@@ -1403,6 +1424,8 @@ using_well_founded { dec_tac := pgame_wf_tac }
 lemma identical.add_left {x y₁ y₂} (hy : y₁ ≡ y₂) : x + y₁ ≡ x + y₂ :=
 (x.add_comm y₁).trans (hy.add_right.trans (y₂.add_comm x))
 
+/-- If `w` has the same moves as `x` and `y` has the same moves as `z`,
+then `w + y` has the same moves as `x + z`. -/
 lemma identical.add {x₁ x₂ y₁ y₂ : pgame.{u}} (hx : x₁ ≡ x₂) (hy : y₁ ≡ y₂) : x₁ + y₁ ≡ x₂ + y₂ :=
 hx.add_right.trans hy.add_left
 
@@ -1440,6 +1463,11 @@ instance : has_sub pgame := ⟨λ x y, x + -y⟩
 @[simp] theorem sub_zero (x : pgame) : x - 0 = x + 0 :=
 show x + -0 = x + 0, by rw neg_zero
 
+/-- Use the same name convention as global lemmas. -/
+lemma neg_sub' (x y : pgame.{u}) : -(x - y) = -x - -y := pgame.neg_add _ _
+
+/-- If `w` has the same moves as `x` and `y` has the same moves as `z`,
+then `w - y` has the same moves as `x - z`. -/
 lemma identical.sub {x₁ x₂ y₁ y₂ : pgame.{u}} (hx : x₁ ≡ x₂) (hy : y₁ ≡ y₂) : x₁ - y₁ ≡ x₂ - y₂ :=
 hx.add hy.neg
 

From 307fe76004953aac803a1f3f857419e14f8132ba Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 1 Mar 2023 06:03:28 +0800
Subject: [PATCH 08/22] fix

---
 src/set_theory/game/basic.lean | 18 ++----------------
 1 file changed, 2 insertions(+), 16 deletions(-)

diff --git a/src/set_theory/game/basic.lean b/src/set_theory/game/basic.lean
index ac584251bbe5d..6e4166b6facd9 100644
--- a/src/set_theory/game/basic.lean
+++ b/src/set_theory/game/basic.lean
@@ -343,7 +343,7 @@ instance is_empty_zero_mul_right_moves (x : pgame.{u}) : is_empty (0 * x).right_
 by { cases x, apply sum.is_empty }
 
 /-- `x * 0` has exactly the same moves as `0`. -/
-protected def mul_zero (x : pgame) : x * 0 ≡ 0 := identical_zero _
+protected lemma mul_zero (x : pgame) : x * 0 ≡ 0 := identical_zero _
 
 /-- `x * 0` has exactly the same moves as `0`. -/
 def mul_zero_relabelling (x : pgame) : x * 0 ≡r 0 := relabelling.is_empty _
@@ -355,7 +355,7 @@ theorem mul_zero_equiv (x : pgame) : x * 0 ≈ 0 := (mul_zero_relabelling x).equ
 @quotient.sound _ _ (x * 0) _ x.mul_zero_equiv
 
 /-- `0 * x` has exactly the same moves as `0`. -/
-protected def zero_mul (x : pgame) : 0 * x ≡ 0 := identical_zero _
+protected lemma zero_mul (x : pgame) : 0 * x ≡ 0 := identical_zero _
 
 /-- `0 * x` has exactly the same moves as `0`. -/
 def zero_mul_relabelling (x : pgame) : 0 * x ≡r 0 := relabelling.is_empty _
@@ -503,20 +503,6 @@ def mul_one_relabelling : Π (x : pgame.{u}), x * 1 ≡r x
     (mul_zero_relabelling _)).trans $ add_zero_relabelling _)
 end
 
-/-- `x * 1` has the same moves as `x`. -/
-def mul_one : Π (x : pgame.{u}), x * 1 ≡ x
-| ⟨xl, xr, xL, xR⟩ := begin
-  unfold has_one.one,
-  refine ⟨(equiv.sum_empty _ _).trans (equiv.prod_punit _),
-    (equiv.empty_sum _ _).trans (equiv.prod_punit _), _, _⟩;
-  try { rintro (⟨i, ⟨ ⟩⟩ | ⟨i, ⟨ ⟩⟩) }; try { intro i };
-  dsimp;
-  apply (relabelling.sub_congr (relabelling.refl _) (mul_zero_relabelling _)).trans;
-  rw sub_zero;
-  exact (add_zero_relabelling _).trans (((mul_one_relabelling _).add_congr
-    (mul_zero_relabelling _)).trans $ add_zero_relabelling _)
-end
-
 @[simp] theorem quot_mul_one (x : pgame) : ⟦x * 1⟧ = ⟦x⟧ := quot.sound $ mul_one_relabelling x
 
 /-- `x * 1` is equivalent to `x`. -/

From ec638b9e872dad67d436d617d26d530c79abb998 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 1 Mar 2023 06:40:15 +0800
Subject: [PATCH 09/22] `one_mul` `mul_one`

---
 src/set_theory/game/basic.lean | 20 +++++++++++++++++++-
 src/set_theory/game/pgame.lean |  5 ++++-
 2 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/src/set_theory/game/basic.lean b/src/set_theory/game/basic.lean
index 6e4166b6facd9..a5977885b6df2 100644
--- a/src/set_theory/game/basic.lean
+++ b/src/set_theory/game/basic.lean
@@ -498,11 +498,29 @@ def mul_one_relabelling : Π (x : pgame.{u}), x * 1 ≡r x
   try { rintro (⟨i, ⟨ ⟩⟩ | ⟨i, ⟨ ⟩⟩) }; try { intro i };
   dsimp;
   apply (relabelling.sub_congr (relabelling.refl _) (mul_zero_relabelling _)).trans;
-  rw sub_zero;
+  rw sub_zero_eq_add_zero;
   exact (add_zero_relabelling _).trans (((mul_one_relabelling _).add_congr
     (mul_zero_relabelling _)).trans $ add_zero_relabelling _)
 end
 
+/-- `1 * x` has the same moves as `x`. -/
+def one_mul : Π (x : pgame.{u}), 1 * x ≡ x
+| ⟨xl, xr, xL, xR⟩ := begin
+  refine identical.ext (λ z, _) (λ z, _),
+  { simp_rw [memₗ_mul_iff], dsimp, simp_rw [is_empty.exists_iff, or_false, exists_const],
+    simp_rw [(((((pgame.zero_mul _).add (one_mul _)).trans (pgame.zero_add _)).sub
+      (xL _).zero_mul).trans (pgame.sub_zero _)).congr_right],
+    refl, },
+  { simp_rw [memᵣ_mul_iff], dsimp, simp_rw [is_empty.exists_iff, or_false, exists_const],
+    simp_rw [(((((pgame.zero_mul _).add (one_mul _)).trans (pgame.zero_add _)).sub
+      (xR _).zero_mul).trans (pgame.sub_zero _)).congr_right],
+    refl, },
+end
+using_well_founded { dec_tac := pgame_wf_tac }
+
+/-- `x * 1` has the same moves as `x`. -/
+def mul_one (x : pgame.{u}) : x * 1 ≡ x := (x.mul_comm _).trans x.one_mul
+
 @[simp] theorem quot_mul_one (x : pgame) : ⟦x * 1⟧ = ⟦x⟧ := quot.sound $ mul_one_relabelling x
 
 /-- `x * 1` is equivalent to `x`. -/
diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index d78c9fe2f301a..17b59bdb55f84 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -1460,9 +1460,12 @@ using_well_founded { dec_tac := pgame_wf_tac }
 
 instance : has_sub pgame := ⟨λ x y, x + -y⟩
 
-@[simp] theorem sub_zero (x : pgame) : x - 0 = x + 0 :=
+@[simp] theorem sub_zero_eq_add_zero (x : pgame) : x - 0 = x + 0 :=
 show x + -0 = x + 0, by rw neg_zero
 
+lemma sub_zero (x : pgame) : x - 0 ≡ x :=
+trans (of_eq x.sub_zero_eq_add_zero) x.add_zero
+
 /-- Use the same name convention as global lemmas. -/
 lemma neg_sub' (x y : pgame.{u}) : -(x - y) = -x - -y := pgame.neg_add _ _
 

From a0da9565643f5d3013b127b3d4109d2167f7f2aa Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 1 Mar 2023 06:41:04 +0800
Subject: [PATCH 10/22] no they are lemmas

---
 src/set_theory/game/basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/set_theory/game/basic.lean b/src/set_theory/game/basic.lean
index a5977885b6df2..068ae8bedc3b1 100644
--- a/src/set_theory/game/basic.lean
+++ b/src/set_theory/game/basic.lean
@@ -504,7 +504,7 @@ def mul_one_relabelling : Π (x : pgame.{u}), x * 1 ≡r x
 end
 
 /-- `1 * x` has the same moves as `x`. -/
-def one_mul : Π (x : pgame.{u}), 1 * x ≡ x
+lemma one_mul : Π (x : pgame.{u}), 1 * x ≡ x
 | ⟨xl, xr, xL, xR⟩ := begin
   refine identical.ext (λ z, _) (λ z, _),
   { simp_rw [memₗ_mul_iff], dsimp, simp_rw [is_empty.exists_iff, or_false, exists_const],
@@ -519,7 +519,7 @@ end
 using_well_founded { dec_tac := pgame_wf_tac }
 
 /-- `x * 1` has the same moves as `x`. -/
-def mul_one (x : pgame.{u}) : x * 1 ≡ x := (x.mul_comm _).trans x.one_mul
+lemma mul_one (x : pgame.{u}) : x * 1 ≡ x := (x.mul_comm _).trans x.one_mul
 
 @[simp] theorem quot_mul_one (x : pgame) : ⟦x * 1⟧ = ⟦x⟧ := quot.sound $ mul_one_relabelling x
 

From 178d7013119dcae3496fe19ded417173fcc6fddb Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 1 Mar 2023 07:41:21 +0800
Subject: [PATCH 11/22] inv lemmas

---
 src/set_theory/game/basic.lean | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

diff --git a/src/set_theory/game/basic.lean b/src/set_theory/game/basic.lean
index 068ae8bedc3b1..ea169fcb73494 100644
--- a/src/set_theory/game/basic.lean
+++ b/src/set_theory/game/basic.lean
@@ -146,7 +146,7 @@ but to prove their properties we need to use the abelian group structure of game
 Hence we define them here. -/
 
 /-- The product of `x = {xL | xR}` and `y = {yL | yR}` is
-`{xL*y + x*yL - xL*yL, xR*y + x*yR - xR*yR | xL*y + x*yR - xL*yR, xR*y + x*yL - xR*yL }`. -/
+`{xL*y + x*yL - xL*yL, xR*y + x*yR - xR*yR | xL*y + x*yR - xL*yR, xR*y + x*yL - xR*yL}`. -/
 instance : has_mul pgame.{u} :=
 ⟨λ x y, begin
   induction x with xl xr xL xR IHxl IHxr generalizing y,
@@ -661,6 +661,14 @@ def inv' : pgame → pgame
 theorem zero_lf_inv' : ∀ (x : pgame), 0 ⧏ inv' x
 | ⟨xl, xr, xL, xR⟩ := by { convert lf_mk _ _ inv_ty.zero, refl }
 
+/-- `inv' 0` has exactly the same moves as `1`. -/
+def inv'_zero' : inv' 0 ≡ 1 :=
+begin
+  refine ⟨_, _⟩,
+  { simp_rw [unique.forall_iff, unique.exists_iff, and_self, pgame.inv_val_is_empty], },
+  { simp_rw [is_empty.forall_iff, and_self], },
+end
+
 /-- `inv' 0` has exactly the same moves as `1`. -/
 def inv'_zero : inv' 0 ≡r 1 :=
 begin
@@ -677,6 +685,17 @@ end
 
 theorem inv'_zero_equiv : inv' 0 ≈ 1 := inv'_zero.equiv
 
+/-- `inv' 1` has exactly the same moves as `1`. -/
+def inv'_one' : inv' 1 ≡ (1 : pgame.{u}) :=
+begin
+  haveI inst : is_empty {i : punit.{u+1} // (0 : pgame.{u}) < 0},
+  { rw lt_self_iff_false, apply_instance },
+  refine ⟨_, _⟩,
+  { simp_rw [unique.forall_iff, unique.exists_iff, pgame.inv_val_is_empty, and_self], },
+  { simp_rw [is_empty.forall_iff, and_true, is_empty.exists_iff],
+    exact (@inv_ty.is_empty _ _ inst _).elim, },
+end
+
 /-- `inv' 1` has exactly the same moves as `1`. -/
 def inv'_one : inv' 1 ≡r (1 : pgame.{u}) :=
 begin
@@ -710,6 +729,10 @@ by { classical, exact (if_neg h.lf.not_equiv').trans (if_pos h) }
 theorem inv_eq_of_lf_zero {x : pgame} (h : x ⧏ 0) : x⁻¹ = -inv' (-x) :=
 by { classical, exact (if_neg h.not_equiv).trans (if_neg h.not_gt) }
 
+/-- `1⁻¹` has exactly the same moves as `1`. -/
+def inv_one' : 1⁻¹ ≡ 1 :=
+by { rw inv_eq_of_pos pgame.zero_lt_one, exact inv'_one' }
+
 /-- `1⁻¹` has exactly the same moves as `1`. -/
 def inv_one : 1⁻¹ ≡r 1 :=
 by { rw inv_eq_of_pos pgame.zero_lt_one, exact inv'_one }

From 5e3b5601b55af9771ad95b2d40644298bed83e8a Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 1 Mar 2023 12:13:59 +0800
Subject: [PATCH 12/22] lint

---
 src/set_theory/game/basic.lean | 8 ++++----
 src/set_theory/game/pgame.lean | 1 +
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/set_theory/game/basic.lean b/src/set_theory/game/basic.lean
index ea169fcb73494..9c00dee2f7fb9 100644
--- a/src/set_theory/game/basic.lean
+++ b/src/set_theory/game/basic.lean
@@ -408,7 +408,7 @@ end
 using_well_founded { dec_tac := pgame_wf_tac }
 
 /-- `-x * y` and `-(x * y)` have the same moves. -/
-def neg_mul (x y : pgame.{u}) : -x * y ≡ -(x * y) :=
+lemma neg_mul (x y : pgame.{u}) : -x * y ≡ -(x * y) :=
 ((pgame.mul_comm _ _).trans (of_eq (mul_neg _ _))).trans (pgame.mul_comm _ _).neg
 
 @[simp] theorem quot_neg_mul (x y : pgame) : ⟦-x * y⟧ = -⟦x * y⟧ :=
@@ -662,7 +662,7 @@ theorem zero_lf_inv' : ∀ (x : pgame), 0 ⧏ inv' x
 | ⟨xl, xr, xL, xR⟩ := by { convert lf_mk _ _ inv_ty.zero, refl }
 
 /-- `inv' 0` has exactly the same moves as `1`. -/
-def inv'_zero' : inv' 0 ≡ 1 :=
+lemma inv'_zero' : inv' 0 ≡ 1 :=
 begin
   refine ⟨_, _⟩,
   { simp_rw [unique.forall_iff, unique.exists_iff, and_self, pgame.inv_val_is_empty], },
@@ -686,7 +686,7 @@ end
 theorem inv'_zero_equiv : inv' 0 ≈ 1 := inv'_zero.equiv
 
 /-- `inv' 1` has exactly the same moves as `1`. -/
-def inv'_one' : inv' 1 ≡ (1 : pgame.{u}) :=
+lemma inv'_one' : inv' 1 ≡ (1 : pgame.{u}) :=
 begin
   haveI inst : is_empty {i : punit.{u+1} // (0 : pgame.{u}) < 0},
   { rw lt_self_iff_false, apply_instance },
@@ -730,7 +730,7 @@ theorem inv_eq_of_lf_zero {x : pgame} (h : x ⧏ 0) : x⁻¹ = -inv' (-x) :=
 by { classical, exact (if_neg h.not_equiv).trans (if_neg h.not_gt) }
 
 /-- `1⁻¹` has exactly the same moves as `1`. -/
-def inv_one' : 1⁻¹ ≡ 1 :=
+lemma inv_one' : 1⁻¹ ≡ 1 :=
 by { rw inv_eq_of_pos pgame.zero_lt_one, exact inv'_one' }
 
 /-- `1⁻¹` has exactly the same moves as `1`. -/
diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index 17b59bdb55f84..cffbf09e156b6 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -772,6 +772,7 @@ theorem identical_of_is_empty (x y : pgame)
   [is_empty y.left_moves] [is_empty y.right_moves] : identical x y :=
 identical_iff'.2 $ by simp [forall_exists_rel]
 
+/-- `identical` as a `setoid`. -/
 def identical_setoid : setoid pgame :=
 ⟨identical, identical.refl, λ x y, identical.symm, λ x y z, identical.trans⟩
 

From 2c75ff76fa299c0b930ebdb277d0391cbc35acf5 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 1 Mar 2023 12:24:23 +0800
Subject: [PATCH 13/22] fix universes

---
 src/set_theory/game/basic.lean | 17 ++++++++++-------
 src/set_theory/game/pgame.lean |  2 +-
 2 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/set_theory/game/basic.lean b/src/set_theory/game/basic.lean
index 9c00dee2f7fb9..9a9eb1d35051a 100644
--- a/src/set_theory/game/basic.lean
+++ b/src/set_theory/game/basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Reid Barton, Mario Carneiro, Isabel Longbottom, Scott Morrison, Apurva Nakade
+Authors: Reid Barton, Mario Carneiro, Isabel Longbottom, Scott Morrison, Apurva Nakade, Yuyang Zhao
 -/
 import set_theory.game.pgame
 import tactic.abel
@@ -662,10 +662,11 @@ theorem zero_lf_inv' : ∀ (x : pgame), 0 ⧏ inv' x
 | ⟨xl, xr, xL, xR⟩ := by { convert lf_mk _ _ inv_ty.zero, refl }
 
 /-- `inv' 0` has exactly the same moves as `1`. -/
-lemma inv'_zero' : inv' 0 ≡ 1 :=
+lemma inv'_zero' : inv' 0 ≡ (1 : pgame.{u}) :=
 begin
   refine ⟨_, _⟩,
-  { simp_rw [unique.forall_iff, unique.exists_iff, and_self, pgame.inv_val_is_empty], },
+  { simp_rw [unique.forall_iff, unique.exists_iff, and_self, pgame.inv_val_is_empty],
+    exact identical_zero _, },
   { simp_rw [is_empty.forall_iff, and_self], },
 end
 
@@ -685,15 +686,17 @@ end
 
 theorem inv'_zero_equiv : inv' 0 ≈ 1 := inv'_zero.equiv
 
+universe v
+
 /-- `inv' 1` has exactly the same moves as `1`. -/
-lemma inv'_one' : inv' 1 ≡ (1 : pgame.{u}) :=
+lemma inv'_one' : inv'.{u} 1 ≡ 1 :=
 begin
   haveI inst : is_empty {i : punit.{u+1} // (0 : pgame.{u}) < 0},
   { rw lt_self_iff_false, apply_instance },
   refine ⟨_, _⟩,
-  { simp_rw [unique.forall_iff, unique.exists_iff, pgame.inv_val_is_empty, and_self], },
-  { simp_rw [is_empty.forall_iff, and_true, is_empty.exists_iff],
-    exact (@inv_ty.is_empty _ _ inst _).elim, },
+  { simp_rw [unique.forall_iff, unique.exists_iff, pgame.inv_val_is_empty, and_self],
+    exact identical_zero _, },
+  { simp_rw [is_empty.forall_iff, and_true], },
 end
 
 /-- `inv' 1` has exactly the same moves as `1`. -/
diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index cffbf09e156b6..af9fb9185efd6 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Reid Barton, Mario Carneiro, Isabel Longbottom, Scott Morrison
+Authors: Reid Barton, Mario Carneiro, Isabel Longbottom, Scott Morrison, Yuyang Zhao
 -/
 import data.fin.basic
 import data.list.basic

From 1b83e5c216a3256eca7250d9b47028da972e942f Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 1 Mar 2023 20:50:13 +0800
Subject: [PATCH 14/22] docs

---
 src/set_theory/game/pgame.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index af9fb9185efd6..fa13ba40400ad 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -687,7 +687,10 @@ end
 end pgame
 
 -- This can also used for golf `Set.equiv` lemmas, but I'm not sure where to put it.
-/-- An auxiliary definition for `pgame.identical` -/
+/-- An auxiliary definition for `pgame.identical`.
+
+`forall_exists_rel r s t` says that for every `s i` there is some `t j` such that `r (s i) (t j)`,
+and for every `t j` there is some `s i` such that `r (s i) (t j)`. -/
 def forall_exists_rel {ι₁ ι₂ α₁ α₂ : Type*} (r : α₁ → α₂ → Prop) (s : ι₁ → α₁) (t : ι₂ → α₂) :=
   (∀ i, ∃ j, r (s i) (t j)) ∧ (∀ j, ∃ i, r (s i) (t j))
 

From 51e4766bd2619d82d6c802ce6e565ea561deaf14 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 29 Mar 2023 15:12:00 +0800
Subject: [PATCH 15/22] docs suggestion
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
---
 src/set_theory/game/pgame.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index fa13ba40400ad..fb8ea4eba66bc 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -21,7 +21,8 @@ types (thought of as indexing the possible moves for the players Left and Right)
 functions out of these types to `pgame` (thought of as describing the resulting game after making a
 move).
 
-Combinatorial games themselves, as a quotient of pregames, are constructed in `basic.lean`.
+Combinatorial games themselves, as a quotient of pregames, are constructed in
+`set_theory.game.basic`.
 
 ## Conway induction
 

From 272c2183982d4ebefeb78103c6824a2920da64a4 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 29 Mar 2023 23:46:14 +0800
Subject: [PATCH 16/22] docs suggestion

---
 src/set_theory/game/pgame.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index fb8ea4eba66bc..4e5f639bb5fb4 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -687,7 +687,7 @@ end
 
 end pgame
 
--- This can also used for golf `Set.equiv` lemmas, but I'm not sure where to put it.
+-- This can also used to golf `pSet.equiv` lemmas, but I'm not sure where to put it.
 /-- An auxiliary definition for `pgame.identical`.
 
 `forall_exists_rel r s t` says that for every `s i` there is some `t j` such that `r (s i) (t j)`,

From abaff14de02ce09c3f2ffd374e93280d419a02b5 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Wed, 29 Mar 2023 23:51:57 +0800
Subject: [PATCH 17/22] : (

---
 src/set_theory/game/pgame.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index 4e5f639bb5fb4..217035099c004 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -687,7 +687,7 @@ end
 
 end pgame
 
--- This can also used to golf `pSet.equiv` lemmas, but I'm not sure where to put it.
+-- This can also be used to golf `pSet.equiv` lemmas, but I'm not sure where to put it.
 /-- An auxiliary definition for `pgame.identical`.
 
 `forall_exists_rel r s t` says that for every `s i` there is some `t j` such that `r (s i) (t j)`,

From 5677ecc089e91f9e6b1cb366f3562d695762f624 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Thu, 30 Mar 2023 20:26:54 +0800
Subject: [PATCH 18/22] suggestion
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
---
 src/set_theory/game/pgame.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index 217035099c004..ba3e3656e86b5 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -1472,7 +1472,7 @@ lemma sub_zero (x : pgame) : x - 0 ≡ x :=
 trans (of_eq x.sub_zero_eq_add_zero) x.add_zero
 
 /-- Use the same name convention as global lemmas. -/
-lemma neg_sub' (x y : pgame.{u}) : -(x - y) = -x - -y := pgame.neg_add _ _
+protected lemma neg_sub' (x y : pgame.{u}) : -(x - y) = -x - -y := pgame.neg_add _ _
 
 /-- If `w` has the same moves as `x` and `y` has the same moves as `z`,
 then `w - y` has the same moves as `x - z`. -/

From 0ee1c7f83b9860ee959a5f38e1fb3ba1857093b0 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Thu, 30 Mar 2023 21:04:07 +0800
Subject: [PATCH 19/22] suggestions

---
 src/set_theory/game/pgame.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index ba3e3656e86b5..0226b22ecf99b 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -1062,11 +1062,11 @@ lemma move_right_neg_symm' {x : pgame} (i) :
 by simp
 
 lemma memₗ_neg_iff : Π {x y : pgame},
-  x ∈ₗ -y ↔ (∃ i, x ≡ -(y.move_right i))
+  x ∈ₗ -y ↔ ∃ i, x ≡ -y.move_right i
 | (mk xl xr xL xR) (mk yl yr yL yR) := iff.rfl
 
 lemma memᵣ_neg_iff : Π {x y : pgame},
-  x ∈ᵣ -y ↔ (∃ i, x ≡ -(y.move_left i))
+  x ∈ᵣ -y ↔ ∃ i, x ≡ -y.move_left i
 | (mk xl xr xL xR) (mk yl yr yL yR) := iff.rfl
 
 /-- If `x` has the same moves as `y`, then `-x` has the sames moves as `-y`. -/
@@ -1077,12 +1077,12 @@ lemma identical.neg : Π {x₁ x₂ : pgame.{u}} (hx : x₁ ≡ x₂), -x₁ ≡
 using_well_founded { dec_tac := pgame_wf_tac }
 
 lemma memₗ_neg_iff' : Π {x y : pgame},
-  x ∈ₗ -y ↔ (∃ z ∈ᵣ y, x ≡ -z)
+  x ∈ₗ -y ↔ ∃ z ∈ᵣ y, x ≡ -z
 | (mk xl xr xL xR) (mk yl yr yL yR) := memₗ_neg_iff.trans
   ⟨λ ⟨i, hi⟩, ⟨_, ⟨_, refl _⟩, hi⟩, λ ⟨_, ⟨i, hi⟩, h⟩, ⟨i, h.trans hi.neg⟩⟩
 
 lemma memᵣ_neg_iff' : Π {x y : pgame},
-  x ∈ᵣ -y ↔ (∃ z ∈ₗ y, x ≡ -z)
+  x ∈ᵣ -y ↔ ∃ z ∈ₗ y, x ≡ -z
 | (mk xl xr xL xR) (mk yl yr yL yR) := memᵣ_neg_iff.trans
   ⟨λ ⟨i, hi⟩, ⟨_, ⟨_, refl _⟩, hi⟩, λ ⟨_, ⟨i, hi⟩, h⟩, ⟨i, h.trans hi.neg⟩⟩
 
@@ -1468,7 +1468,7 @@ instance : has_sub pgame := ⟨λ x y, x + -y⟩
 @[simp] theorem sub_zero_eq_add_zero (x : pgame) : x - 0 = x + 0 :=
 show x + -0 = x + 0, by rw neg_zero
 
-lemma sub_zero (x : pgame) : x - 0 ≡ x :=
+protected lemma sub_zero (x : pgame) : x - 0 ≡ x :=
 trans (of_eq x.sub_zero_eq_add_zero) x.add_zero
 
 /-- Use the same name convention as global lemmas. -/

From 76a8748343b9cc18beb791d24f9fc0428f5dd195 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Thu, 30 Mar 2023 21:12:05 +0800
Subject: [PATCH 20/22] .exists

---
 src/set_theory/game/basic.lean |  8 ++++----
 src/set_theory/game/pgame.lean | 12 ++++++------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/set_theory/game/basic.lean b/src/set_theory/game/basic.lean
index 9a9eb1d35051a..eea7fa5e6b68c 100644
--- a/src/set_theory/game/basic.lean
+++ b/src/set_theory/game/basic.lean
@@ -263,7 +263,7 @@ begin
   { apply hr }
 end
 
-lemma exists_left_moves_mul {x y : pgame.{u}} {p : (x * y).left_moves → Prop} :
+lemma left_moves_mul.exists {x y : pgame.{u}} {p : (x * y).left_moves → Prop} :
   (∃ i, p i) ↔
     (∃ i j, p (to_left_moves_mul (sum.inl (i, j)))) ∨
     (∃ i j, p (to_left_moves_mul (sum.inr (i, j)))) :=
@@ -274,7 +274,7 @@ begin
   { rintros (⟨i, j, h⟩ | ⟨i, j, h⟩), exacts [⟨_, h⟩, ⟨_, h⟩], },
 end
 
-lemma exists_right_moves_mul {x y : pgame.{u}} {p : (x * y).right_moves → Prop} :
+lemma right_moves_mul.exists {x y : pgame.{u}} {p : (x * y).right_moves → Prop} :
   (∃ i, p i) ↔
     (∃ i j, p (to_right_moves_mul (sum.inl (i, j)))) ∨
     (∃ i j, p (to_right_moves_mul (sum.inr (i, j)))) :=
@@ -289,13 +289,13 @@ lemma memₗ_mul_iff : Π {x y₁ y₂ : pgame},
   x ∈ₗ y₁ * y₂ ↔
     (∃ i j, x ≡ y₁.move_left i * y₂ + y₁ * y₂.move_left j - y₁.move_left i * y₂.move_left j) ∨
     (∃ i j, x ≡ y₁.move_right i * y₂ + y₁ * y₂.move_right j - y₁.move_right i * y₂.move_right j)
-| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := exists_left_moves_mul
+| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := left_moves_mul.exists
 
 lemma memᵣ_mul_iff : Π {x y₁ y₂ : pgame},
   x ∈ᵣ y₁ * y₂ ↔
     (∃ i j, x ≡ y₁.move_left i * y₂ + y₁ * y₂.move_right j - y₁.move_left i * y₂.move_right j) ∨
     (∃ i j, x ≡ y₁.move_right i * y₂ + y₁ * y₂.move_left j - y₁.move_right i * y₂.move_left j)
-| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := exists_right_moves_mul
+| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := right_moves_mul.exists
 
 /-- `x * y` and `y * x` have the same moves. -/
 protected lemma mul_comm : Π (x y : pgame.{u}), x * y ≡ y * x
diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index 0226b22ecf99b..cb478f5331280 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -1314,7 +1314,7 @@ instance is_empty_nat_right_moves : ∀ n : ℕ, is_empty (right_moves n)
   apply_instance
 end
 
-lemma exists_left_moves_add {x y : pgame.{u}} {p : (x + y).left_moves → Prop} :
+lemma left_moves_add.exists {x y : pgame.{u}} {p : (x + y).left_moves → Prop} :
   (∃ i, p i) ↔
     (∃ i, p (to_left_moves_add (sum.inl i))) ∨ (∃ i, p (to_left_moves_add (sum.inr i))) :=
 begin
@@ -1324,7 +1324,7 @@ begin
   { rintros (⟨i, hi⟩ | ⟨i, hi⟩), exacts [⟨_, hi⟩, ⟨_, hi⟩], }
 end
 
-lemma exists_right_moves_add {x y : pgame.{u}} {p : (x + y).right_moves → Prop} :
+lemma right_moves_add.exists {x y : pgame.{u}} {p : (x + y).right_moves → Prop} :
   (∃ i, p i) ↔
     (∃ i, p (to_right_moves_add (sum.inl i))) ∨ (∃ i, p (to_right_moves_add (sum.inr i))) :=
 begin
@@ -1336,11 +1336,11 @@ end
 
 lemma memₗ_add_iff : Π {x y₁ y₂ : pgame},
   x ∈ₗ y₁ + y₂ ↔ (∃ i, x ≡ (y₁.move_left i) + y₂) ∨ (∃ i, x ≡ y₁ + (y₂.move_left i))
-| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := exists_left_moves_add
+| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := left_moves_add.exists
 
 lemma memᵣ_add_iff : Π {x y₁ y₂ : pgame},
   x ∈ᵣ y₁ + y₂ ↔ (∃ i, x ≡ (y₁.move_right i) + y₂) ∨ (∃ i, x ≡ y₁ + (y₂.move_right i))
-| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := exists_right_moves_add
+| (mk xl xr xL xR) (mk y₁l y₁r y₁L y₁R) (mk y₂l y₂r y₂L y₂R) := right_moves_add.exists
 
 /-- `x + y` has exactly the same moves as `y + x`. -/
 protected lemma add_comm : Π (x y : pgame.{u}), x + y ≡ y + x
@@ -1357,9 +1357,9 @@ using_well_founded { dec_tac := pgame_wf_tac }
 protected lemma add_assoc : Π (x y z : pgame.{u}), x + y + z ≡ x + (y + z)
 | (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR) := begin
   refine identical.ext (λ z, _) (λ z, _),
-  { simp_rw [memₗ_add_iff, exists_left_moves_add, or.assoc,
+  { simp_rw [memₗ_add_iff, left_moves_add.exists, or.assoc,
       add_move_left_inl, add_move_left_inr, (add_assoc _ _ _).congr_right], },
-  { simp_rw [memᵣ_add_iff, exists_right_moves_add, or.assoc,
+  { simp_rw [memᵣ_add_iff, right_moves_add.exists, or.assoc,
       add_move_right_inl, add_move_right_inr, (add_assoc _ _ _).congr_right], },
 end
 using_well_founded { dec_tac := pgame_wf_tac }

From bd9bdbaf169beb636c9367050bc1012567ee68d7 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Thu, 30 Mar 2023 21:36:38 +0800
Subject: [PATCH 21/22] suggestion
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
---
 src/set_theory/game/pgame.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index cb478f5331280..b9a62893c2a5b 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -765,7 +765,7 @@ pgame.rec_on x $ λ xl xr xL xR IHL IHR y, pgame.cases_on y $ λ yl yr yL yR ⟨
 @[symm] protected theorem identical.symm {x y} : x ≡ y → y ≡ x :=
 (identical.refl y).euc
 
-protected theorem identical.comm {x y} : x ≡ y ↔ y ≡ x :=
+protected theorem identical_comm {x y} : x ≡ y ↔ y ≡ x :=
 ⟨identical.symm, identical.symm⟩
 
 @[trans] protected theorem identical.trans {x y z} (h₁ : x ≡ y) (h₂ : y ≡ z) : x ≡ z :=

From a3529ba324740ad459ed9429322ca37dd670b8c8 Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Thu, 30 Mar 2023 22:28:07 +0800
Subject: [PATCH 22/22] fix

---
 src/set_theory/game/pgame.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index b9a62893c2a5b..cd80f9fb21a53 100644
--- a/src/set_theory/game/pgame.lean
+++ b/src/set_theory/game/pgame.lean
@@ -765,7 +765,7 @@ pgame.rec_on x $ λ xl xr xL xR IHL IHR y, pgame.cases_on y $ λ yl yr yL yR ⟨
 @[symm] protected theorem identical.symm {x y} : x ≡ y → y ≡ x :=
 (identical.refl y).euc
 
-protected theorem identical_comm {x y} : x ≡ y ↔ y ≡ x :=
+theorem identical_comm {x y} : x ≡ y ↔ y ≡ x :=
 ⟨identical.symm, identical.symm⟩
 
 @[trans] protected theorem identical.trans {x y z} (h₁ : x ≡ y) (h₂ : y ≡ z) : x ≡ z :=
@@ -799,7 +799,7 @@ theorem identical_iff : Π {x y : pgame}, x ≡ y ↔
     ((∀ i, (x.move_right i) ∈ᵣ y) ∧ (∀ j, (y.move_right j) ∈ᵣ x))
 | (mk _ _ _ _) (mk _ _ _ _) := begin
   convert identical_iff';
-  exact pi_congr (λ i, propext (exists_congr $ λ j, by rw [identical.comm])),
+  exact pi_congr (λ i, propext (exists_congr $ λ j, by rw [identical_comm])),
 end
 
 theorem memₗ.congr_right : Π {x y : pgame.{u}},