refactor: separate out PGame.relabelling

Mathlib.lean

@@ -4816,6 +4816,7 @@ import Mathlib.SetTheory.Game.Impartial
 import Mathlib.SetTheory.Game.Nim
 import Mathlib.SetTheory.Game.Ordinal
 import Mathlib.SetTheory.Game.PGame
+import Mathlib.SetTheory.Game.Relabelling
 import Mathlib.SetTheory.Game.Short
 import Mathlib.SetTheory.Game.State
 import Mathlib.SetTheory.Lists

Mathlib/SetTheory/Game/Basic.lean

@@ -389,22 +389,8 @@ protected lemma mul_comm (x y : PGame) : x * y ≡ y * x :=
         (PGame.add_comm _ _)).sub (PGame.mul_comm _ _))
   termination_by (x, y)
 
-/-- `x * y` and `y * x` have the same moves. -/
-def mulCommRelabelling (x y : PGame.{u}) : x * y ≡r y * x :=
-  match x, y with
-  | ⟨xl, xr, xL, xR⟩, ⟨yl, yr, yL, yR⟩ => by
-    refine ⟨Equiv.sumCongr (Equiv.prodComm _ _) (Equiv.prodComm _ _),
-      (Equiv.sumComm _ _).trans (Equiv.sumCongr (Equiv.prodComm _ _) (Equiv.prodComm _ _)), ?_, ?_⟩
-      <;>
-    rintro (⟨i, j⟩ | ⟨i, j⟩) <;>
-    { dsimp
-      exact ((addCommRelabelling _ _).trans <|
-        (mulCommRelabelling _ _).addCongr (mulCommRelabelling _ _)).subCongr
-        (mulCommRelabelling _ _) }
-  termination_by (x, y)
-
 theorem quot_mul_comm (x y : PGame.{u}) : (⟦x * y⟧ : Game) = ⟦y * x⟧ :=
-  game_eq (mulCommRelabelling x y).equiv
+  game_eq (x.mul_comm y).equiv
 
 /-- `x * y` is equivalent to `y * x`. -/
 theorem mul_comm_equiv (x y : PGame) : x * y ≈ y * x :=
@@ -427,13 +413,9 @@ instance isEmpty_rightMoves_mul (x y : PGame.{u})
 /-- `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 mulZeroRelabelling (x : PGame) : x * 0 ≡r 0 :=
-  Relabelling.isEmpty _
-
 /-- `x * 0` is equivalent to `0`. -/
 theorem mul_zero_equiv (x : PGame) : x * 0 ≈ 0 :=
-  (mulZeroRelabelling x).equiv
+  x.mul_zero.equiv
 
 @[simp]
 theorem quot_mul_zero (x : PGame) : (⟦x * 0⟧ : Game) = 0 :=
@@ -442,37 +424,14 @@ theorem quot_mul_zero (x : PGame) : (⟦x * 0⟧ : Game) = 0 :=
 /-- `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 zeroMulRelabelling (x : PGame) : 0 * x ≡r 0 :=
-  Relabelling.isEmpty _
-
 /-- `0 * x` is equivalent to `0`. -/
 theorem zero_mul_equiv (x : PGame) : 0 * x ≈ 0 :=
-  (zeroMulRelabelling x).equiv
+  x.zero_mul.equiv
 
 @[simp]
 theorem quot_zero_mul (x : PGame) : (⟦0 * x⟧ : Game) = 0 :=
   game_eq x.zero_mul_equiv
 
-/-- `-x * y` and `-(x * y)` have the same moves. -/
-def negMulRelabelling (x y : PGame.{u}) : -x * y ≡r -(x * y) :=
-  match x, y with
-  | ⟨xl, xr, xL, xR⟩, ⟨yl, yr, yL, yR⟩ => by
-      refine ⟨Equiv.sumComm _ _, Equiv.sumComm _ _, ?_, ?_⟩ <;>
-      rintro (⟨i, j⟩ | ⟨i, j⟩) <;>
-      · dsimp
-        apply ((negAddRelabelling _ _).trans _).symm
-        apply ((negAddRelabelling _ _).trans (Relabelling.addCongr _ _)).subCongr
-        -- Porting note: we used to just do `<;> exact (negMulRelabelling _ _).symm` from here.
-        · exact (negMulRelabelling _ _).symm
-        · exact (negMulRelabelling _ _).symm
-        -- Porting note: not sure what has gone wrong here.
-        -- The goal is hideous here, and the `exact` doesn't work,
-        -- but if we just `change` it to look like the mathlib3 goal then we're fine!?
-        change -(mk xl xr xL xR * _) ≡r _
-        exact (negMulRelabelling _ _).symm
-  termination_by (x, y)
-
 /-- `x * -y` and `-(x * y)` have the same moves. -/
 @[simp]
 lemma mul_neg (x y : PGame) : x * -y = -(x * y) :=
@@ -492,14 +451,10 @@ lemma neg_mul (x y : PGame) : -x * y ≡ -(x * y) :=
 
 @[simp]
 theorem quot_neg_mul (x y : PGame) : (⟦-x * y⟧ : Game) = -⟦x * y⟧ :=
-  game_eq (negMulRelabelling x y).equiv
-
-/-- `x * -y` and `-(x * y)` have the same moves. -/
-def mulNegRelabelling (x y : PGame) : x * -y ≡r -(x * y) :=
-  (mulCommRelabelling x _).trans <| (negMulRelabelling _ x).trans (mulCommRelabelling y x).negCongr
+  game_eq (x.neg_mul y).equiv
 
 theorem quot_mul_neg (x y : PGame) : ⟦x * -y⟧ = (-⟦x * y⟧ : Game) :=
-  game_eq (mulNegRelabelling x y).equiv
+  game_eq (x.mul_neg y ▸ Setoid.refl _) -- Porting note: was `of_eq (x.mul_neg y)`
 
 theorem quot_neg_mul_neg (x y : PGame) : ⟦-x * -y⟧ = (⟦x * y⟧ : Game) := by simp
 
@@ -622,23 +577,6 @@ theorem quot_right_distrib_sub (x y z : PGame) : (⟦(y - z) * x⟧ : Game) = 
   change (⟦(y + -z) * x⟧ : Game) = ⟦y * x⟧ + -⟦z * x⟧
   rw [quot_right_distrib, quot_neg_mul]
 
-/-- `x * 1` has the same moves as `x`. -/
-def mulOneRelabelling : ∀ x : PGame.{u}, x * 1 ≡r x
-  | ⟨xl, xr, xL, xR⟩ => by
-    -- Porting note: the next four lines were just `unfold has_one.one,`
-    show _ * One.one ≡r _
-    unfold One.one
-    unfold instOnePGame
-    change mk _ _ _ _ * mk _ _ _ _ ≡r _
-    refine ⟨(Equiv.sumEmpty _ _).trans (Equiv.prodPUnit _),
-      (Equiv.emptySum _ _).trans (Equiv.prodPUnit _), ?_, ?_⟩ <;>
-    (try rintro (⟨i, ⟨⟩⟩ | ⟨i, ⟨⟩⟩)) <;>
-    { dsimp
-      apply (Relabelling.subCongr (Relabelling.refl _) (mulZeroRelabelling _)).trans
-      rw [sub_zero_eq_add_zero]
-      exact (addZeroRelabelling _).trans <|
-        (((mulOneRelabelling _).addCongr (mulZeroRelabelling _)).trans <| addZeroRelabelling _) }
-
 /-- `1 * x` has the same moves as `x`. -/
 protected lemma one_mul : ∀ (x : PGame), 1 * x ≡ x
   | ⟨xl, xr, xL, xR⟩ => by
@@ -653,19 +591,15 @@ protected lemma mul_one (x : PGame) : x * 1 ≡ x := (x.mul_comm _).trans x.one_
 
 @[simp]
 theorem quot_mul_one (x : PGame) : (⟦x * 1⟧ : Game) = ⟦x⟧ :=
-  game_eq <| PGame.Relabelling.equiv <| mulOneRelabelling x
+  game_eq x.mul_one.equiv
 
 /-- `x * 1` is equivalent to `x`. -/
 theorem mul_one_equiv (x : PGame) : x * 1 ≈ x :=
   Quotient.exact <| quot_mul_one x
 
-/-- `1 * x` has the same moves as `x`. -/
-def oneMulRelabelling (x : PGame) : 1 * x ≡r x :=
-  (mulCommRelabelling 1 x).trans <| mulOneRelabelling x
-
 @[simp]
 theorem quot_one_mul (x : PGame) : (⟦1 * x⟧ : Game) = ⟦x⟧ :=
-  game_eq <| PGame.Relabelling.equiv <| oneMulRelabelling x
+  game_eq x.one_mul.equiv
 
 /-- `1 * x` is equivalent to `x`. -/
 theorem one_mul_equiv (x : PGame) : 1 * x ≈ x :=
@@ -949,44 +883,15 @@ theorem zero_lf_inv' : ∀ x : PGame, 0 ⧏ inv' x
     convert lf_mk _ _ InvTy.zero
     rfl
 
-/-- `inv' 0` has exactly the same moves as `1`. -/
-def inv'Zero : inv' 0 ≡r 1 := by
-  change mk _ _ _ _ ≡r 1
-  refine ⟨?_, ?_, fun i => ?_, IsEmpty.elim ?_⟩
-  · apply Equiv.equivPUnit (InvTy _ _ _)
-  · apply Equiv.equivPEmpty (InvTy _ _ _)
-  · -- Porting note: we added `rfl` after the `simp`
-    -- (because `simp` now uses `rfl` only at reducible transparency)
-    -- Can we improve the simp set so it is not needed?
-    simp; rfl
-  · dsimp
-    infer_instance
-
-theorem inv'_zero_equiv : inv' 0 ≈ 1 :=
-  inv'Zero.equiv
-
 /-- `inv' 1` has exactly the same moves as `1`. -/
 lemma inv'_one : inv' 1 ≡ 1 := by
   rw [Identical.ext_iff]
   constructor
   · simp [memₗ_def, inv', isEmpty_subtype]
   · simp [memᵣ_def, inv', isEmpty_subtype]
 
-/-- `inv' 1` has exactly the same moves as `1`. -/
-def inv'One : inv' 1 ≡r (1 : PGame.{u}) := by
-  change Relabelling (mk _ _ _ _) 1
-  have : IsEmpty { _i : PUnit.{u + 1} // (0 : PGame.{u}) < 0 } := by
-    rw [lt_self_iff_false]
-    infer_instance
-  refine ⟨?_, ?_, fun i => ?_, IsEmpty.elim ?_⟩ <;> dsimp
-  · apply Equiv.equivPUnit
-  · apply Equiv.equivOfIsEmpty
-  · -- Porting note: had to add `rfl`, because `simp` only uses the built-in `rfl`.
-    simp; rfl
-  · infer_instance
-
 theorem inv'_one_equiv : inv' 1 ≈ 1 :=
-  inv'One.equiv
+  inv'_one.equiv
 
 /-- The inverse of a pre-game in terms of the inverse on positive pre-games. -/
 noncomputable instance : Inv PGame :=
@@ -1012,13 +917,8 @@ 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 invOne : 1⁻¹ ≡r 1 := by
-  rw [inv_eq_of_pos PGame.zero_lt_one]
-  exact inv'One
-
 theorem inv_one_equiv : (1⁻¹ : PGame) ≈ 1 :=
-  invOne.equiv
+  inv_one.equiv
 
 end PGame
 

Mathlib/SetTheory/Game/Birthday.lean

@@ -76,18 +76,18 @@ theorem lt_birthday_iff {x : PGame} {o : Ordinal} :
     · exact hi.trans_lt (birthday_moveLeft_lt i)
     · exact hi.trans_lt (birthday_moveRight_lt i)
 
-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 => by
     unfold birthday
     congr 1
     all_goals
       apply lsub_eq_of_range_eq.{u, u, u}
       ext i; constructor
     all_goals rintro ⟨j, rfl⟩
-    · exact ⟨_, (r.moveLeft j).birthday_congr.symm⟩
-    · exact ⟨_, (r.moveLeftSymm j).birthday_congr⟩
-    · exact ⟨_, (r.moveRight j).birthday_congr.symm⟩
-    · exact ⟨_, (r.moveRightSymm j).birthday_congr⟩
+    · exact (r.moveLeft j).imp (fun _ hi ↦ hi.birthday_congr.symm)
+    · exact (r.moveLeft_symm j).imp (fun _ hi ↦ hi.birthday_congr)
+    · exact (r.moveRight j).imp (fun _ hi ↦ hi.birthday_congr.symm)
+    · exact (r.moveRight_symm j).imp (fun _ hi ↦ hi.birthday_congr)
 
 @[simp]
 theorem birthday_eq_zero {x : PGame} :

Mathlib/SetTheory/Game/Impartial.lean

@@ -26,11 +26,11 @@ namespace PGame
 
 /-- The definition for an impartial game, defined using Conway induction. -/
 def ImpartialAux (G : PGame) : Prop :=
-  (G ≈ -G) ∧ (∀ i, ImpartialAux (G.moveLeft i)) ∧ ∀ j, ImpartialAux (G.moveRight j)
+  (G ≡ -G) ∧ (∀ i, ImpartialAux (G.moveLeft i)) ∧ ∀ j, ImpartialAux (G.moveRight j)
 termination_by G
 
 theorem impartialAux_def {G : PGame} : G.ImpartialAux ↔
-    (G ≈ -G) ∧ (∀ i, ImpartialAux (G.moveLeft i)) ∧ ∀ j, ImpartialAux (G.moveRight j) := by
+    (G ≡ -G) ∧ (∀ i, ImpartialAux (G.moveLeft i)) ∧ ∀ j, ImpartialAux (G.moveRight j) := by
   rw [ImpartialAux]
 
 /-- A typeclass on impartial games. -/
@@ -41,7 +41,7 @@ theorem impartial_iff_aux {G : PGame} : G.Impartial ↔ G.ImpartialAux :=
   ⟨fun h => h.1, fun h => ⟨h⟩⟩
 
 theorem impartial_def {G : PGame} :
-    G.Impartial ↔ (G ≈ -G) ∧ (∀ i, Impartial (G.moveLeft i)) ∧ ∀ j, Impartial (G.moveRight j) := by
+    G.Impartial ↔ (G ≡ -G) ∧ (∀ i, Impartial (G.moveLeft i)) ∧ ∀ j, Impartial (G.moveRight j) := by
   simpa only [impartial_iff_aux] using impartialAux_def
 
 namespace Impartial
@@ -54,12 +54,12 @@ instance impartial_star : Impartial star := by
   rw [impartial_def]
   simpa using Impartial.impartial_zero
 
-theorem neg_equiv_self (G : PGame) [h : G.Impartial] : G ≈ -G :=
+theorem neg_identical_self (G : PGame) [h : G.Impartial] : G ≡ -G :=
   (impartial_def.1 h).1
 
 @[simp]
-theorem mk'_neg_equiv_self (G : PGame) [G.Impartial] : -(⟦G⟧ : Game) = ⟦G⟧ :=
-  game_eq (Equiv.symm (neg_equiv_self G))
+theorem mk'_neg_equiv_self (G : PGame) [G.Impartial] : -(⟦G⟧ : Quotient setoid) = ⟦G⟧ :=
+  game_eq (neg_identical_self G).symm.equiv
 
 instance moveLeft_impartial {G : PGame} [h : G.Impartial] (i : G.LeftMoves) :
     (G.moveLeft i).Impartial :=
@@ -69,16 +69,17 @@ instance moveRight_impartial {G : PGame} [h : G.Impartial] (j : G.RightMoves) :
     (G.moveRight j).Impartial :=
   (impartial_def.1 h).2.2 j
 
-theorem impartial_congr {G H : PGame} (e : G ≡r H) [G.Impartial] : H.Impartial :=
+theorem impartial_congr {G H : PGame} (e : G ≡ H) [G.Impartial] : H.Impartial :=
   impartial_def.2
-    ⟨Equiv.trans e.symm.equiv (Equiv.trans (neg_equiv_self G) (neg_equiv_neg_iff.2 e.equiv)),
-      fun i => impartial_congr (e.moveLeftSymm i), fun j => impartial_congr (e.moveRightSymm j)⟩
-termination_by G
+    ⟨e.symm.trans ((neg_identical_self G).trans e.neg),
+      fun i => (e.moveLeft_symm i).elim fun _ ↦ (impartial_congr ·),
+      fun j => (e.moveRight_symm j).elim fun _ ↦ (impartial_congr ·)⟩
+termination_by (G, H)
 
 instance impartial_add (G H : PGame) [G.Impartial] [H.Impartial] : (G + H).Impartial := by
   rw [impartial_def]
-  refine ⟨Equiv.trans (add_congr (neg_equiv_self G) (neg_equiv_self _))
-      (Equiv.symm (negAddRelabelling _ _).equiv), fun k => ?_, fun k => ?_⟩
+  refine ⟨((neg_identical_self G).add (neg_identical_self _)).trans <|
+      of_eq (PGame.neg_add _ _).symm, fun k => ?_, fun k => ?_⟩
   · apply leftMoves_add_cases k
     all_goals
       intro i; simp only [add_moveLeft_inl, add_moveLeft_inr]
@@ -93,7 +94,7 @@ instance impartial_neg (G : PGame) [G.Impartial] : (-G).Impartial := by
   rw [impartial_def]
   refine ⟨?_, fun i => ?_, fun i => ?_⟩
   · rw [neg_neg]
-    exact Equiv.symm (neg_equiv_self G)
+    exact (neg_identical_self G).symm
   · rw [moveLeft_neg]
     exact impartial_neg _
   · rw [moveRight_neg]
@@ -105,13 +106,13 @@ variable (G : PGame) [Impartial G]
 theorem nonpos : ¬0 < G := by
   intro h
   have h' := neg_lt_neg_iff.2 h
-  rw [neg_zero, lt_congr_left (Equiv.symm (neg_equiv_self G))] at h'
+  rw [neg_zero, lt_congr_left (neg_identical_self G).symm.equiv] at h'
   exact (h.trans h').false
 
 theorem nonneg : ¬G < 0 := by
   intro h
   have h' := neg_lt_neg_iff.2 h
-  rw [neg_zero, lt_congr_right (Equiv.symm (neg_equiv_self G))] at h'
+  rw [neg_zero, lt_congr_right (neg_identical_self G).symm.equiv] at h'
   exact (h.trans h').false
 
 /-- In an impartial game, either the first player always wins, or the second player always wins. -/
@@ -131,7 +132,7 @@ theorem not_fuzzy_zero_iff : ¬G ‖ 0 ↔ (G ≈ 0) :=
   ⟨(equiv_or_fuzzy_zero G).resolve_right, Equiv.not_fuzzy⟩
 
 theorem add_self : G + G ≈ 0 :=
-  Equiv.trans (add_congr_left (neg_equiv_self G)) (neg_add_cancel_equiv G)
+  Equiv.trans (add_congr_left (neg_identical_self G).equiv) (neg_add_cancel_equiv G)
 
 @[simp]
 theorem mk'_add_self : (⟦G⟧ : Game) + ⟦G⟧ = 0 :=
@@ -148,10 +149,10 @@ theorem equiv_iff_add_equiv_zero' (H : PGame) : (G ≈ H) ↔ (G + H ≈ 0) := b
     Eq.comm, quot_zero]
 
 theorem le_zero_iff {G : PGame} [G.Impartial] : G ≤ 0 ↔ 0 ≤ G := by
-  rw [← zero_le_neg_iff, le_congr_right (neg_equiv_self G)]
+  rw [← zero_le_neg_iff, le_congr_right (neg_identical_self G).equiv]
 
 theorem lf_zero_iff {G : PGame} [G.Impartial] : G ⧏ 0 ↔ 0 ⧏ G := by
-  rw [← zero_lf_neg_iff, lf_congr_right (neg_equiv_self G)]
+  rw [← zero_lf_neg_iff, lf_congr_right (neg_identical_self G).equiv]
 
 theorem equiv_zero_iff_le : (G ≈ 0) ↔ G ≤ 0 :=
   ⟨And.left, fun h => ⟨h, le_zero_iff.1 h⟩⟩

Mathlib/SetTheory/Game/Nim.lean

@@ -126,11 +126,11 @@ instance isEmpty_nim_zero_rightMoves : IsEmpty (nim 0).RightMoves := by
   exact isEmpty_toType_zero
 
 /-- `nim 0` has exactly the same moves as `0`. -/
-def nimZeroRelabelling : nim 0 ≡r 0 :=
-  Relabelling.isEmpty _
+lemma nim_zero : nim 0 ≡ 0 :=
+  identical_zero _
 
 theorem nim_zero_equiv : nim 0 ≈ 0 :=
-  Equiv.isEmpty _
+  equiv_zero _
 
 noncomputable instance uniqueNimOneLeftMoves : Unique (nim 1).LeftMoves :=
   (Equiv.cast <| leftMoves_nim 1).unique
@@ -163,14 +163,15 @@ theorem nim_one_moveLeft (x) : (nim 1).moveLeft x = nim 0 := by simp
 theorem nim_one_moveRight (x) : (nim 1).moveRight x = nim 0 := by simp
 
 /-- `nim 1` has exactly the same moves as `star`. -/
-def nimOneRelabelling : nim 1 ≡r star := by
-  rw [nim_def]
-  refine ⟨?_, ?_, fun i => ?_, fun j => ?_⟩
-  any_goals dsimp; apply Equiv.ofUnique
-  all_goals simpa [enumIsoToType] using nimZeroRelabelling
+lemma nim_one : nim.{u} 1 ≡ star.{u} := by
+  refine Identical.ext (fun z ↦ ?_) (fun z ↦ ?_)
+  · simp_rw [memₗ_def, nim_one_moveLeft, Unique.exists_iff, star_moveLeft]
+    exact Identical.congr_right nim_zero
+  · simp_rw [memᵣ_def, nim_one_moveRight, Unique.exists_iff, star_moveRight]
+    exact Identical.congr_right nim_zero
 
 theorem nim_one_equiv : nim 1 ≈ star :=
-  nimOneRelabelling.equiv
+  nim_one.equiv
 
 @[simp]
 theorem nim_birthday (o : Ordinal) : (nim o).birthday = o := by
@@ -189,7 +190,7 @@ theorem neg_nim (o : Ordinal) : -nim o = nim o := by
 instance nim_impartial (o : Ordinal) : Impartial (nim o) := by
   induction' o using Ordinal.induction with o IH
   rw [impartial_def, neg_nim]
-  refine ⟨equiv_rfl, fun i => ?_, fun i => ?_⟩ <;> simpa using IH _ (typein_lt_self _)
+  refine ⟨refl _, fun i => ?_, fun i => ?_⟩ <;> simpa using IH _ (typein_lt_self _)
 
 theorem nim_fuzzy_zero_of_ne_zero {o : Ordinal} (ho : o ≠ 0) : nim o ‖ 0 := by
   rw [Impartial.fuzzy_zero_iff_lf, lf_zero_le]