chore: move Game to SetTheory.Game (#6365)

move `Game` and `PGame` into namespace `SetTheory` as `_root_.Game` might collide with other definitions (e.g. in projects depending on mathlib)

Mathlib/SetTheory/Game/Birthday.lean

@@ -17,11 +17,11 @@ prove the basic properties about these.
 
 # Main declarations
 
-- `PGame.birthday`: The birthday of a pre-game.
+- `SetTheory.PGame.birthday`: The birthday of a pre-game.
 
 # Todo
 
-- Define the birthdays of `Game`s and `Surreal`s.
+- Define the birthdays of `SetTheory.Game`s and `Surreal`s.
 - Characterize the birthdays of basic arithmetical operations.
 -/
 
@@ -30,6 +30,8 @@ universe u
 
 open Ordinal
 
+namespace SetTheory
+
 open scoped NaturalOps PGame
 
 namespace PGame
@@ -40,23 +42,23 @@ constructed. -/
 noncomputable def birthday : PGame.{u} → Ordinal.{u}
   | ⟨_, _, xL, xR⟩ =>
     max (lsub.{u, u} fun i => birthday (xL i)) (lsub.{u, u} fun i => birthday (xR i))
-#align pgame.birthday PGame.birthday
+#align pgame.birthday SetTheory.PGame.birthday
 
 theorem birthday_def (x : PGame) :
     birthday x =
       max (lsub.{u, u} fun i => birthday (x.moveLeft i))
         (lsub.{u, u} fun i => birthday (x.moveRight i)) := by
   cases x; rw [birthday]; rfl
-#align pgame.birthday_def PGame.birthday_def
+#align pgame.birthday_def SetTheory.PGame.birthday_def
 
 theorem birthday_moveLeft_lt {x : PGame} (i : x.LeftMoves) : (x.moveLeft i).birthday < x.birthday :=
   by cases x; rw [birthday]; exact lt_max_of_lt_left (lt_lsub _ i)
-#align pgame.birthday_move_left_lt PGame.birthday_moveLeft_lt
+#align pgame.birthday_move_left_lt SetTheory.PGame.birthday_moveLeft_lt
 
 theorem birthday_moveRight_lt {x : PGame} (i : x.RightMoves) :
     (x.moveRight i).birthday < x.birthday := by
   cases x; rw [birthday]; exact lt_max_of_lt_right (lt_lsub _ i)
-#align pgame.birthday_move_right_lt PGame.birthday_moveRight_lt
+#align pgame.birthday_move_right_lt SetTheory.PGame.birthday_moveRight_lt
 
 theorem lt_birthday_iff {x : PGame} {o : Ordinal} :
     o < x.birthday ↔
@@ -73,7 +75,7 @@ theorem lt_birthday_iff {x : PGame} {o : Ordinal} :
   · rintro (⟨i, hi⟩ | ⟨i, hi⟩)
     · exact hi.trans_lt (birthday_moveLeft_lt i)
     · exact hi.trans_lt (birthday_moveRight_lt i)
-#align pgame.lt_birthday_iff PGame.lt_birthday_iff
+#align pgame.lt_birthday_iff SetTheory.PGame.lt_birthday_iff
 
 theorem Relabelling.birthday_congr : ∀ {x y : PGame.{u}}, x ≡r y → birthday x = birthday y
   | ⟨xl, xr, xL, xR⟩, ⟨yl, yr, yL, yR⟩, r => by
@@ -88,32 +90,32 @@ theorem Relabelling.birthday_congr : ∀ {x y : PGame.{u}}, x ≡r y → birthda
     · exact ⟨_, (r.moveRight j).birthday_congr.symm⟩
     · exact ⟨_, (r.moveRightSymm j).birthday_congr⟩
 termination_by birthday_congr x y _ => (x, y)
-#align pgame.relabelling.birthday_congr PGame.Relabelling.birthday_congr
+#align pgame.relabelling.birthday_congr SetTheory.PGame.Relabelling.birthday_congr
 
 @[simp]
 theorem birthday_eq_zero {x : PGame} :
     birthday x = 0 ↔ IsEmpty x.LeftMoves ∧ IsEmpty x.RightMoves := by
   rw [birthday_def, max_eq_zero, lsub_eq_zero_iff, lsub_eq_zero_iff]
-#align pgame.birthday_eq_zero PGame.birthday_eq_zero
+#align pgame.birthday_eq_zero SetTheory.PGame.birthday_eq_zero
 
 @[simp]
 theorem birthday_zero : birthday 0 = 0 := by simp [inferInstanceAs (IsEmpty PEmpty)]
-#align pgame.birthday_zero PGame.birthday_zero
+#align pgame.birthday_zero SetTheory.PGame.birthday_zero
 
 @[simp]
 theorem birthday_one : birthday 1 = 1 := by rw [birthday_def]; simp
-#align pgame.birthday_one PGame.birthday_one
+#align pgame.birthday_one SetTheory.PGame.birthday_one
 
 @[simp]
 theorem birthday_star : birthday star = 1 := by rw [birthday_def]; simp
-#align pgame.birthday_star PGame.birthday_star
+#align pgame.birthday_star SetTheory.PGame.birthday_star
 
 @[simp]
 theorem neg_birthday : ∀ x : PGame, (-x).birthday = x.birthday
   | ⟨xl, xr, xL, xR⟩ => by
     rw [birthday_def, birthday_def, max_comm]
     congr <;> funext <;> apply neg_birthday
-#align pgame.neg_birthday PGame.neg_birthday
+#align pgame.neg_birthday SetTheory.PGame.neg_birthday
 
 @[simp]
 theorem toPGame_birthday (o : Ordinal) : o.toPGame.birthday = o := by
@@ -124,21 +126,21 @@ theorem toPGame_birthday (o : Ordinal) : o.toPGame.birthday = o := by
   conv_rhs => rw [← lsub_typein o]
   congr with x
   exact IH _ (typein_lt_self x)
-#align pgame.to_pgame_birthday PGame.toPGame_birthday
+#align pgame.to_pgame_birthday SetTheory.PGame.toPGame_birthday
 
 theorem le_birthday : ∀ x : PGame, x ≤ x.birthday.toPGame
   | ⟨xl, _, xL, _⟩ =>
     le_def.2
       ⟨fun i =>
         Or.inl ⟨toLeftMovesToPGame ⟨_, birthday_moveLeft_lt i⟩, by simp [le_birthday (xL i)]⟩,
         isEmptyElim⟩
-#align pgame.le_birthday PGame.le_birthday
+#align pgame.le_birthday SetTheory.PGame.le_birthday
 
 variable (a b x : PGame.{u})
 
 theorem neg_birthday_le : -x.birthday.toPGame ≤ x := by
   simpa only [neg_birthday, ← neg_le_iff] using le_birthday (-x)
-#align pgame.neg_birthday_le PGame.neg_birthday_le
+#align pgame.neg_birthday_le SetTheory.PGame.neg_birthday_le
 
 @[simp]
 theorem birthday_add : ∀ x y : PGame.{u}, (x + y).birthday = x.birthday ♯ y.birthday
@@ -169,30 +171,30 @@ theorem birthday_add : ∀ x y : PGame.{u}, (x + y).birthday = x.birthday ♯ y.
     · exact lt_max_of_lt_left ((nadd_le_nadd_left hj _).trans_lt (lt_lsub _ _))
     · exact lt_max_of_lt_right ((nadd_le_nadd_left hj _).trans_lt (lt_lsub _ _))
 termination_by birthday_add a b => (a, b)
-#align pgame.birthday_add PGame.birthday_add
+#align pgame.birthday_add SetTheory.PGame.birthday_add
 
 theorem birthday_add_zero : (a + 0).birthday = a.birthday := by simp
-#align pgame.birthday_add_zero PGame.birthday_add_zero
+#align pgame.birthday_add_zero SetTheory.PGame.birthday_add_zero
 
 theorem birthday_zero_add : (0 + a).birthday = a.birthday := by simp
-#align pgame.birthday_zero_add PGame.birthday_zero_add
+#align pgame.birthday_zero_add SetTheory.PGame.birthday_zero_add
 
 theorem birthday_add_one : (a + 1).birthday = Order.succ a.birthday := by simp
-#align pgame.birthday_add_one PGame.birthday_add_one
+#align pgame.birthday_add_one SetTheory.PGame.birthday_add_one
 
 theorem birthday_one_add : (1 + a).birthday = Order.succ a.birthday := by simp
-#align pgame.birthday_one_add PGame.birthday_one_add
+#align pgame.birthday_one_add SetTheory.PGame.birthday_one_add
 
 @[simp]
 theorem birthday_nat_cast : ∀ n : ℕ, birthday n = n
   | 0 => birthday_zero
   | n + 1 => by simp [birthday_nat_cast]
-#align pgame.birthday_nat_cast PGame.birthday_nat_cast
+#align pgame.birthday_nat_cast SetTheory.PGame.birthday_nat_cast
 
 theorem birthday_add_nat (n : ℕ) : (a + n).birthday = a.birthday + n := by simp
-#align pgame.birthday_add_nat PGame.birthday_add_nat
+#align pgame.birthday_add_nat SetTheory.PGame.birthday_add_nat
 
 theorem birthday_nat_add (n : ℕ) : (↑n + a).birthday = a.birthday + n := by simp
-#align pgame.birthday_nat_add PGame.birthday_nat_add
+#align pgame.birthday_nat_add SetTheory.PGame.birthday_nat_add
 
 end PGame

Mathlib/SetTheory/Game/Domineering.lean

@@ -21,6 +21,7 @@ Specifically to domineering, we need the fact that
 disjoint parts of the chessboard give sums of games.
 -/
 
+namespace SetTheory
 
 namespace PGame
 
@@ -32,13 +33,13 @@ open Function
 @[simps!]
 def shiftUp : ℤ × ℤ ≃ ℤ × ℤ :=
   (Equiv.refl ℤ).prodCongr (Equiv.addRight (1 : ℤ))
-#align pgame.domineering.shift_up PGame.Domineering.shiftUp
+#align pgame.domineering.shift_up SetTheory.PGame.Domineering.shiftUp
 
 /-- The equivalence `(x, y) ↦ (x+1, y)`. -/
 @[simps!]
 def shiftRight : ℤ × ℤ ≃ ℤ × ℤ :=
   (Equiv.addRight (1 : ℤ)).prodCongr (Equiv.refl ℤ)
-#align pgame.domineering.shift_right PGame.Domineering.shiftRight
+#align pgame.domineering.shift_right SetTheory.PGame.Domineering.shiftRight
 
 /-- A Domineering board is an arbitrary finite subset of `ℤ × ℤ`. -/
 -- Porting note: `reducible` cannot be `local`. For now there are no dependents of this file so
@@ -47,89 +48,89 @@ def shiftRight : ℤ × ℤ ≃ ℤ × ℤ :=
 def Board :=
   Finset (ℤ × ℤ)
 deriving Inhabited
-#align pgame.domineering.board PGame.Domineering.Board
+#align pgame.domineering.board SetTheory.PGame.Domineering.Board
 
 /-- Left can play anywhere that a square and the square below it are open. -/
 def left (b : Board) : Finset (ℤ × ℤ) :=
   b ∩ b.map shiftUp
-#align pgame.domineering.left PGame.Domineering.left
+#align pgame.domineering.left SetTheory.PGame.Domineering.left
 
 /-- Right can play anywhere that a square and the square to the left are open. -/
 def right (b : Board) : Finset (ℤ × ℤ) :=
   b ∩ b.map shiftRight
-#align pgame.domineering.right PGame.Domineering.right
+#align pgame.domineering.right SetTheory.PGame.Domineering.right
 
 theorem mem_left {b : Board} (x : ℤ × ℤ) : x ∈ left b ↔ x ∈ b ∧ (x.1, x.2 - 1) ∈ b :=
   Finset.mem_inter.trans (and_congr Iff.rfl Finset.mem_map_equiv)
-#align pgame.domineering.mem_left PGame.Domineering.mem_left
+#align pgame.domineering.mem_left SetTheory.PGame.Domineering.mem_left
 
 theorem mem_right {b : Board} (x : ℤ × ℤ) : x ∈ right b ↔ x ∈ b ∧ (x.1 - 1, x.2) ∈ b :=
   Finset.mem_inter.trans (and_congr Iff.rfl Finset.mem_map_equiv)
-#align pgame.domineering.mem_right PGame.Domineering.mem_right
+#align pgame.domineering.mem_right SetTheory.PGame.Domineering.mem_right
 
 /-- After Left moves, two vertically adjacent squares are removed from the board. -/
 def moveLeft (b : Board) (m : ℤ × ℤ) : Board :=
   (b.erase m).erase (m.1, m.2 - 1)
-#align pgame.domineering.move_left PGame.Domineering.moveLeft
+#align pgame.domineering.move_left SetTheory.PGame.Domineering.moveLeft
 
 /-- After Left moves, two horizontally adjacent squares are removed from the board. -/
 def moveRight (b : Board) (m : ℤ × ℤ) : Board :=
   (b.erase m).erase (m.1 - 1, m.2)
-#align pgame.domineering.move_right PGame.Domineering.moveRight
+#align pgame.domineering.move_right SetTheory.PGame.Domineering.moveRight
 
 theorem fst_pred_mem_erase_of_mem_right {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) :
     (m.1 - 1, m.2) ∈ b.erase m := by
   rw [mem_right] at h
   apply Finset.mem_erase_of_ne_of_mem _ h.2
   exact ne_of_apply_ne Prod.fst (pred_ne_self m.1)
-#align pgame.domineering.fst_pred_mem_erase_of_mem_right PGame.Domineering.fst_pred_mem_erase_of_mem_right
+#align pgame.domineering.fst_pred_mem_erase_of_mem_right SetTheory.PGame.Domineering.fst_pred_mem_erase_of_mem_right
 
 theorem snd_pred_mem_erase_of_mem_left {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) :
     (m.1, m.2 - 1) ∈ b.erase m := by
   rw [mem_left] at h
   apply Finset.mem_erase_of_ne_of_mem _ h.2
   exact ne_of_apply_ne Prod.snd (pred_ne_self m.2)
-#align pgame.domineering.snd_pred_mem_erase_of_mem_left PGame.Domineering.snd_pred_mem_erase_of_mem_left
+#align pgame.domineering.snd_pred_mem_erase_of_mem_left SetTheory.PGame.Domineering.snd_pred_mem_erase_of_mem_left
 
 theorem card_of_mem_left {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) : 2 ≤ Finset.card b := by
   have w₁ : m ∈ b := (Finset.mem_inter.1 h).1
   have w₂ : (m.1, m.2 - 1) ∈ b.erase m := snd_pred_mem_erase_of_mem_left h
   have i₁ := Finset.card_erase_lt_of_mem w₁
   have i₂ := Nat.lt_of_le_of_lt (Nat.zero_le _) (Finset.card_erase_lt_of_mem w₂)
   exact Nat.lt_of_le_of_lt i₂ i₁
-#align pgame.domineering.card_of_mem_left PGame.Domineering.card_of_mem_left
+#align pgame.domineering.card_of_mem_left SetTheory.PGame.Domineering.card_of_mem_left
 
 theorem card_of_mem_right {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) : 2 ≤ Finset.card b := by
   have w₁ : m ∈ b := (Finset.mem_inter.1 h).1
   have w₂ := fst_pred_mem_erase_of_mem_right h
   have i₁ := Finset.card_erase_lt_of_mem w₁
   have i₂ := Nat.lt_of_le_of_lt (Nat.zero_le _) (Finset.card_erase_lt_of_mem w₂)
   exact Nat.lt_of_le_of_lt i₂ i₁
-#align pgame.domineering.card_of_mem_right PGame.Domineering.card_of_mem_right
+#align pgame.domineering.card_of_mem_right SetTheory.PGame.Domineering.card_of_mem_right
 
 theorem moveLeft_card {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) :
     Finset.card (moveLeft b m) + 2 = Finset.card b := by
   dsimp [moveLeft]
   rw [Finset.card_erase_of_mem (snd_pred_mem_erase_of_mem_left h)]
   rw [Finset.card_erase_of_mem (Finset.mem_of_mem_inter_left h)]
   exact tsub_add_cancel_of_le (card_of_mem_left h)
-#align pgame.domineering.move_left_card PGame.Domineering.moveLeft_card
+#align pgame.domineering.move_left_card SetTheory.PGame.Domineering.moveLeft_card
 
 theorem moveRight_card {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) :
     Finset.card (moveRight b m) + 2 = Finset.card b := by
   dsimp [moveRight]
   rw [Finset.card_erase_of_mem (fst_pred_mem_erase_of_mem_right h)]
   rw [Finset.card_erase_of_mem (Finset.mem_of_mem_inter_left h)]
   exact tsub_add_cancel_of_le (card_of_mem_right h)
-#align pgame.domineering.move_right_card PGame.Domineering.moveRight_card
+#align pgame.domineering.move_right_card SetTheory.PGame.Domineering.moveRight_card
 
 theorem moveLeft_smaller {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) :
     Finset.card (moveLeft b m) / 2 < Finset.card b / 2 := by simp [← moveLeft_card h, lt_add_one]
-#align pgame.domineering.move_left_smaller PGame.Domineering.moveLeft_smaller
+#align pgame.domineering.move_left_smaller SetTheory.PGame.Domineering.moveLeft_smaller
 
 theorem moveRight_smaller {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) :
     Finset.card (moveRight b m) / 2 < Finset.card b / 2 := by simp [← moveRight_card h, lt_add_one]
-#align pgame.domineering.move_right_smaller PGame.Domineering.moveRight_smaller
+#align pgame.domineering.move_right_smaller SetTheory.PGame.Domineering.moveRight_smaller
 
 /-- The instance describing allowed moves on a Domineering board. -/
 instance state : State Board where
@@ -144,38 +145,38 @@ instance state : State Board where
     simp only [Finset.mem_image, Prod.exists] at m
     rcases m with ⟨_, _, ⟨h, rfl⟩⟩
     exact moveRight_smaller h
-#align pgame.domineering.state PGame.Domineering.state
+#align pgame.domineering.state SetTheory.PGame.Domineering.state
 
 end Domineering
 
 /-- Construct a pre-game from a Domineering board. -/
 def domineering (b : Domineering.Board) : PGame :=
   PGame.ofState b
-#align pgame.domineering PGame.domineering
+#align pgame.domineering SetTheory.PGame.domineering
 
 /-- All games of Domineering are short, because each move removes two squares. -/
 instance shortDomineering (b : Domineering.Board) : Short (domineering b) := by
   dsimp [domineering]
   infer_instance
-#align pgame.short_domineering PGame.shortDomineering
+#align pgame.short_domineering SetTheory.PGame.shortDomineering
 
 /-- The Domineering board with two squares arranged vertically, in which Left has the only move. -/
 def domineering.one :=
   domineering [(0, 0), (0, 1)].toFinset
-#align pgame.domineering.one PGame.domineering.one
+#align pgame.domineering.one SetTheory.PGame.domineering.one
 
 /-- The `L` shaped Domineering board, in which Left is exactly half a move ahead. -/
 def domineering.L :=
   domineering [(0, 2), (0, 1), (0, 0), (1, 0)].toFinset
 set_option linter.uppercaseLean3 false in
-#align pgame.domineering.L PGame.domineering.L
+#align pgame.domineering.L SetTheory.PGame.domineering.L
 
 instance shortOne : Short domineering.one := by dsimp [domineering.one]; infer_instance
-#align pgame.short_one PGame.shortOne
+#align pgame.short_one SetTheory.PGame.shortOne
 
 instance shortL : Short domineering.L := by dsimp [domineering.L]; infer_instance
 set_option linter.uppercaseLean3 false in
-#align pgame.short_L PGame.shortL
+#align pgame.short_L SetTheory.PGame.shortL
 
 -- The VM can play small games successfully:
 -- #eval decide (domineering.one ≈ 1)