refactor(set_theory/game/*): remove relabelling

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,
@@ -263,20 +263,59 @@ 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) := 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) := exists_right_moves_mul
+
 /-- `x * y` and `y * x` have the same moves. -/
-def mul_comm_relabelling : Π (x y : pgame.{u}), x * y ≡r y * x
+protected lemma mul_comm : Π (x y : pgame.{u}), x * y ≡ y * x
 | ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ := begin
-  refine ⟨equiv.sum_congr (equiv.prod_comm _ _) (equiv.prod_comm _ _),
-    (equiv.sum_comm _ _).trans (equiv.sum_congr (equiv.prod_comm _ _) (equiv.prod_comm _ _)), _, _⟩;
-  rintro (⟨i, j⟩ | ⟨i, j⟩);
-  dsimp;
-  exact ((add_comm_relabelling _ _).trans $ (mul_comm_relabelling _ _).add_congr
-    (mul_comm_relabelling _ _)).sub_congr (mul_comm_relabelling _ _)
+  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 }
 
 theorem quot_mul_comm (x y : pgame.{u}) : ⟦x * y⟧ = ⟦y * x⟧ :=
-quot.sound (mul_comm_relabelling x y).equiv
+quot.sound (x.mul_comm y).equiv
 
 /-- `x * y` is equivalent to `y * x`. -/
 theorem mul_comm_equiv (x y : pgame) : x * y ≈ y * x :=
@@ -292,45 +331,61 @@ 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`. -/
-def mul_zero_relabelling (x : pgame) : x * 0 ≡r 0 := relabelling.is_empty _
+protected lemma mul_zero (x : pgame) : x * 0 ≡ 0 := identical_zero _
 
 /-- `x * 0` is equivalent to `0`. -/
-theorem mul_zero_equiv (x : pgame) : x * 0 ≈ 0 := (mul_zero_relabelling x).equiv
+theorem mul_zero_equiv (x : pgame) : x * 0 ≈ 0 := x.mul_zero.equiv
 
 @[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`. -/
-def zero_mul_relabelling (x : pgame) : 0 * x ≡r 0 := relabelling.is_empty _
+protected lemma zero_mul (x : pgame) : 0 * x ≡ 0 := identical_zero _
 
 /-- `0 * x` is equivalent to `0`. -/
-theorem zero_mul_equiv (x : pgame) : 0 * x ≈ 0 := (zero_mul_relabelling x).equiv
+theorem zero_mul_equiv (x : pgame) : 0 * x ≈ 0 := x.zero_mul.equiv
 
 @[simp] theorem quot_zero_mul (x : pgame) : ⟦0 * x⟧ = ⟦0⟧ :=
 @quotient.sound _ _ (0 * x) _ x.zero_mul_equiv
 
-/-- `-x * y` and `-(x * y)` have the same moves. -/
-def neg_mul_relabelling : Π (x y : pgame.{u}), -x * y ≡r -(x * y)
-| ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ := begin
-  refine ⟨equiv.sum_comm _ _, equiv.sum_comm _ _, _, _⟩;
-  rintro (⟨i, j⟩ | ⟨i, j⟩);
-  dsimp;
-  apply ((neg_add_relabelling _ _).trans _).symm;
-  apply ((neg_add_relabelling _ _).trans (relabelling.add_congr _ _)).sub_congr;
-  exact (neg_mul_relabelling _ _).symm
+/-- `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 }
 
-@[simp] theorem quot_neg_mul (x y : pgame) : ⟦-x * y⟧ = -⟦x * y⟧ :=
-quot.sound (neg_mul_relabelling x y).equiv
+/-- `-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
 
-/-- `x * -y` and `-(x * y)` have the same moves. -/
-def mul_neg_relabelling (x y : pgame) : x * -y ≡r -(x * y) :=
-(mul_comm_relabelling x _).trans $
-  (neg_mul_relabelling _ x).trans (mul_comm_relabelling y x).neg_congr
+@[simp] theorem quot_neg_mul (x y : pgame) : ⟦-x * y⟧ = -⟦x * y⟧ :=
+quot.sound (neg_mul x y).equiv
 
 @[simp] theorem quot_mul_neg (x y : pgame) : ⟦x * -y⟧ = -⟦x * y⟧ :=
-quot.sound (mul_neg_relabelling x y).equiv
+quot.sound (of_eq (mul_neg x y))
 
 @[simp] theorem quot_left_distrib : Π (x y z : pgame), ⟦x * (y + z)⟧ = ⟦x * y⟧ + ⟦x * z⟧
 | (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR) :=
@@ -399,33 +454,33 @@ quotient.exact $ quot_right_distrib _ _ _
 @[simp] theorem quot_right_distrib_sub (x y z : pgame) : ⟦(y - z) * x⟧ = ⟦y * x⟧ - ⟦z * x⟧ :=
 by { change ⟦(y + -z) * x⟧ = ⟦y * x⟧ + -⟦z * x⟧, rw [quot_right_distrib, quot_neg_mul] }
 
-/-- `x * 1` has the same moves as `x`. -/
-def mul_one_relabelling : Π (x : pgame.{u}), x * 1 ≡r x
+/-- `1 * x` has the same moves as `x`. -/
+lemma one_mul : Π (x : pgame.{u}), 1 * x ≡ 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 _)
+  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 }
 
-@[simp] theorem quot_mul_one (x : pgame) : ⟦x * 1⟧ = ⟦x⟧ := quot.sound $ mul_one_relabelling x
+@[simp] theorem quot_one_mul (x : pgame) : ⟦1 * x⟧ = ⟦x⟧ := quot.sound $ (one_mul x).equiv
 
-/-- `x * 1` is equivalent to `x`. -/
-theorem mul_one_equiv (x : pgame) : x * 1 ≈ x := quotient.exact $ quot_mul_one x
+/-- `1 * x` is equivalent to `x`. -/
+theorem one_mul_equiv (x : pgame) : 1 * x ≈ x := quotient.exact $ quot_one_mul x
 
-/-- `1 * x` has the same moves as `x`. -/
-def one_mul_relabelling (x : pgame) : 1 * x ≡r x :=
-(mul_comm_relabelling 1 x).trans $ mul_one_relabelling x
+/-- `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_one_mul (x : pgame) : ⟦1 * x⟧ = ⟦x⟧ := quot.sound $ one_mul_relabelling x
+@[simp] theorem quot_mul_one (x : pgame) : ⟦x * 1⟧ = ⟦x⟧ := quot.sound $ (mul_one x).equiv
 
-/-- `1 * x` is equivalent to `x`. -/
-theorem one_mul_equiv (x : pgame) : 1 * x ≈ x := quotient.exact $ quot_one_mul x
+/-- `x * 1` is equivalent to `x`. -/
+theorem mul_one_equiv (x : pgame) : x * 1 ≈ x := quotient.exact $ quot_mul_one x
 
 theorem quot_mul_assoc : Π (x y z : pgame), ⟦x * y * z⟧ = ⟦x * (y * z)⟧
 | (mk xl xr xL xR) (mk yl yr yL yR) (mk zl zr zL zR) :=
@@ -554,32 +609,24 @@ 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 ≡r 1 :=
+def inv'_zero : inv' 0 ≡ 1 :=
 begin
-  change mk _ _ _ _ ≡r 1,
-  refine ⟨_, _, λ i, _, is_empty.elim _⟩,
-  { apply equiv.equiv_punit (inv_ty _ _ _),
-    apply_instance },
-  { apply equiv.equiv_pempty (inv_ty _ _ _),
-    apply_instance },
-  { simp },
-  { dsimp,
-    apply_instance }
+  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
 
 theorem inv'_zero_equiv : inv' 0 ≈ 1 := inv'_zero.equiv
 
 /-- `inv' 1` has exactly the same moves as `1`. -/
-def inv'_one : inv' 1 ≡r (1 : pgame.{u}) :=
+def inv'_one : inv' 1 ≡ (1 : pgame.{u}) :=
 begin
-  change relabelling (mk _ _ _ _) 1,
-  haveI : is_empty {i : punit.{u+1} // (0 : pgame.{u}) < 0},
+  haveI inst : is_empty {i : punit.{u+1} // (0 : pgame.{u}) < 0},
   { rw lt_self_iff_false, apply_instance },
-  refine ⟨_, _, λ i, _, is_empty.elim _⟩; dsimp,
-  { apply equiv.equiv_punit },
-  { apply equiv.equiv_of_is_empty },
-  { simp },
-  { 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
 
 theorem inv'_one_equiv : inv' 1 ≈ 1 := inv'_one.equiv
@@ -603,7 +650,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⁻¹ ≡r 1 :=
+def inv_one : 1⁻¹ ≡ 1 :=
 by { rw inv_eq_of_pos pgame.zero_lt_one, exact inv'_one }
 
 theorem inv_one_equiv : 1⁻¹ ≈ 1 := inv_one.equiv

src/set_theory/game/birthday.lean

@@ -69,18 +69,18 @@ begin
     { exact hi.trans_lt (birthday_move_right_lt i) } }
 end
 
-theorem relabelling.birthday_congr : ∀ {x y : pgame.{u}}, x ≡r y → birthday x = birthday y
+theorem identical.birthday_congr : ∀ {x y : pgame.{u}}, x ≡ y → birthday x = birthday y
 | ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ r := begin
   unfold birthday,
   congr' 1,
   all_goals
   { apply lsub_eq_of_range_eq.{u u u},
     ext i, split },
   all_goals { rintro ⟨j, rfl⟩ },
-  { exact ⟨_, (r.move_left j).birthday_congr.symm⟩ },
-  { exact ⟨_, (r.move_left_symm j).birthday_congr⟩ },
-  { exact ⟨_, (r.move_right j).birthday_congr.symm⟩ },
-  { exact ⟨_, (r.move_right_symm j).birthday_congr⟩ }
+  { exact (r.move_left j).imp (λ i hi, hi.birthday_congr.symm) },
+  { exact (r.move_left_symm j).imp (λ i hi, hi.birthday_congr) },
+  { exact (r.move_right j).imp (λ i hi, hi.birthday_congr.symm) },
+  { exact (r.move_right_symm j).imp (λ i hi, hi.birthday_congr) },
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 

src/set_theory/game/impartial.lean

@@ -62,7 +62,7 @@ instance move_right_impartial {G : pgame} [h : G.impartial] (j : G.right_moves)
   (G.move_right j).impartial :=
 (impartial_def.1 h).2.2 j
 
-theorem impartial_congr : ∀ {G H : pgame} (e : G ≡r H) [G.impartial], H.impartial
+theorem identical_congr : ∀ {G H : pgame} (e : G ≡ H) [G.impartial], H.impartial
 | G H := λ e, begin
   introI h,
   exact impartial_def.2
@@ -77,7 +77,7 @@ begin
   introsI hG hH,
   rw impartial_def,
   refine ⟨(add_congr (neg_equiv_self _) (neg_equiv_self _)).trans
-    (neg_add_relabelling _ _).equiv.symm, λ k, _, λ k, _⟩,
+    (equiv_of_eq (pgame.neg_add _ _)).symm, λ k, _, λ k, _⟩,
   { apply left_moves_add_cases k,
     all_goals
     { intro i, simp only [add_move_left_inl, add_move_left_inr],

src/set_theory/game/nim.lean

@@ -113,7 +113,7 @@ instance is_empty_nim_zero_right_moves : is_empty (nim 0).right_moves :=
 by { rw nim_def, exact ordinal.is_empty_out_zero }
 
 /-- `nim 0` has exactly the same moves as `0`. -/
-def nim_zero_relabelling : nim 0 ≡r 0 := relabelling.is_empty _
+lemma nim_zero_identical : nim 0 ≡ 0 := identical_zero _
 
 theorem nim_zero_equiv : nim 0 ≈ 0 := equiv.is_empty _
 
@@ -146,15 +146,18 @@ theorem nim_one_move_right (x) : (nim 1).move_right x = nim 0 :=
 by simp
 
 /-- `nim 1` has exactly the same moves as `star`. -/
-def nim_one_relabelling : nim 1 ≡r star :=
+lemma nim_one_identical : nim.{u} 1 ≡ star.{u} :=
 begin
-  rw nim_def,
-  refine ⟨_, _, λ i, _, λ j, _⟩,
-  any_goals { dsimp, apply equiv.equiv_of_unique },
-  all_goals { simp, exact nim_zero_relabelling }
+  refine identical.ext (λ z, _) (λ z, _),
+  { unfold memₗ,
+    simp_rw [nim_one_move_left, unique.exists_iff, star_move_left],
+    exact identical.congr_right nim_zero_identical, },
+  { unfold memᵣ,
+    simp_rw [nim_one_move_right, unique.exists_iff, star_move_right],
+    exact identical.congr_right nim_zero_identical, },
 end
 
-theorem nim_one_equiv : nim 1 ≈ star := nim_one_relabelling.equiv
+theorem nim_one_equiv : nim 1 ≈ star := nim_one_identical.equiv
 
 @[simp] lemma nim_birthday (o : ordinal) : (nim o).birthday = o :=
 begin

src/set_theory/game/ordinal.lean

@@ -73,8 +73,8 @@ theorem to_pgame_move_left {o : ordinal} (i) :
 by simp
 
 /-- `0.to_pgame` has the same moves as `0`. -/
-noncomputable def zero_to_pgame_relabelling : to_pgame 0 ≡r 0 :=
-relabelling.is_empty _
+lemma zero_to_pgame : to_pgame 0 ≡ 0 :=
+identical_zero _
 
 noncomputable instance unique_one_to_pgame_left_moves : unique (to_pgame 1).left_moves :=
 (equiv.cast $ to_pgame_left_moves 1).unique
@@ -91,9 +91,14 @@ theorem one_to_pgame_move_left (x) : (to_pgame 1).move_left x = to_pgame 0 :=
 by simp
 
 /-- `1.to_pgame` has the same moves as `1`. -/
-noncomputable def one_to_pgame_relabelling : to_pgame 1 ≡r 1 :=
-⟨equiv.equiv_of_unique _ _, equiv.equiv_of_is_empty _ _,
-  λ i, by simpa using zero_to_pgame_relabelling, is_empty_elim⟩
+lemma one_to_pgame : to_pgame.{u} 1 ≡ (1 : pgame.{u}) :=
+begin
+  refine identical.ext (λ z, _) (λ z, _),
+  { unfold memₗ,
+    simp_rw [one_to_pgame_move_left, unique.exists_iff],
+    exact identical.congr_right zero_to_pgame, },
+  { unfold memᵣ, simp, },
+end
 
 theorem to_pgame_lf {a b : ordinal} (h : a < b) : a.to_pgame ⧏ b.to_pgame :=
 by { convert move_left_lf (to_left_moves_to_pgame ⟨a, h⟩), rw to_pgame_move_left }
@@ -109,7 +114,7 @@ theorem to_pgame_lt {a b : ordinal} (h : a < b) : a.to_pgame < b.to_pgame :=
 ⟨to_pgame_le h.le, to_pgame_lf h⟩
 
 theorem to_pgame_nonneg (a : ordinal) : 0 ≤ a.to_pgame :=
-zero_to_pgame_relabelling.ge.trans $ to_pgame_le $ ordinal.zero_le a
+zero_to_pgame.symm.le.trans $ to_pgame_le $ ordinal.zero_le a
 
 @[simp] theorem to_pgame_lf_iff {a b : ordinal} : a.to_pgame ⧏ b.to_pgame ↔ a < b :=
 ⟨by { contrapose, rw [not_lt, not_lf], exact to_pgame_le }, to_pgame_lf⟩