diff --git a/src/set_theory/game/basic.lean b/src/set_theory/game/basic.lean
index c440ab66e49f4..eea7fa5e6b68c 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
@@ -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,
@@ -263,6 +263,57 @@ begin
   { apply hr }
 end
 
+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)))) :=
+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 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)))) :=
+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) := 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) := 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
+| ⟨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
@@ -291,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 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 _
 
@@ -300,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 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 _
 
@@ -321,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. -/
+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⟧ :=
 quot.sound (neg_mul_relabelling x y).equiv
 
@@ -408,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`. -/
+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],
+    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`. -/
+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
 
 /-- `x * 1` is equivalent to `x`. -/
@@ -553,6 +661,15 @@ 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`. -/
+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],
+    exact identical_zero _, },
+  { 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
@@ -569,6 +686,19 @@ 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'.{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],
+    exact identical_zero _, },
+  { simp_rw [is_empty.forall_iff, and_true], },
+end
+
 /-- `inv' 1` has exactly the same moves as `1`. -/
 def inv'_one : inv' 1 ≡r (1 : pgame.{u}) :=
 begin
@@ -602,6 +732,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`. -/
+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`. -/
 def inv_one : 1⁻¹ ≡r 1 :=
 by { rw inv_eq_of_pos pgame.zero_lt_one, exact inv'_one }
diff --git a/src/set_theory/game/pgame.lean b/src/set_theory/game/pgame.lean
index 3c9a085d0633f..cd80f9fb21a53 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
@@ -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 `game.lean`.
+Combinatorial games themselves, as a quotient of pregames, are constructed in
+`set_theory.game.basic`.
 
 ## Conway induction
 
@@ -129,6 +130,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.
 -/
@@ -672,6 +685,152 @@ begin
   exact lt_or_equiv_or_gt_or_fuzzy x y
 end
 
+end pgame
+
+-- 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)`,
+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))
+
+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
+
+/-! ### 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))) ∧
+    ((∀ i, ∃ j, identical (xR i) (yR j)) ∧ (∀ j, ∃ i, identical (xR i) (yR j)))
+
+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
+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
+
+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]
+
+/-- `identical` as a `setoid`. -/
+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 +1061,31 @@ 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
+
+/-- 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)⟩,
+    ⟨λ 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 +1314,138 @@ instance is_empty_nat_right_moves : ∀ n : ℕ, is_empty (right_moves n)
   apply_instance
 end
 
+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
+  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 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
+  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 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) := 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) := 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
+| (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 }
+
+/-- `(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, _),
+  { 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, 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 }
+
+/-- `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, _),
+  { 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 }
+
+/-- `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
+
+/-- `-(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 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 }
+
+/-- `-(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
+| (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
+
+/-- Any game without left or right moves is identival to 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
+| (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₂ :=
+(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
+
+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
@@ -1149,9 +1465,20 @@ 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
 
+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. -/
+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`. -/
+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 :=