Documentation

Mathlib.SetTheory.Game.PGame

Combinatorial (pre-)games. #

The basic theory of combinatorial games, following Conway's book On Numbers and Games. We construct "pregames", define an ordering and arithmetic operations on them, then show that the operations descend to "games", defined via the equivalence relation p ≈ q ↔ p ≤ q ∧ q ≤ p.

The surreal numbers will be built as a quotient of a subtype of pregames.

A pregame (SetTheory.PGame below) is axiomatised via an inductive type, whose sole constructor takes two types (thought of as indexing the possible moves for the players Left and Right), and a pair of functions out of these types to SetTheory.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.

Conway induction #

By construction, the induction principle for pregames is exactly "Conway induction". That is, to prove some predicate SetTheory.PGame → Prop holds for all pregames, it suffices to prove that for every pregame g, if the predicate holds for every game resulting from making a move, then it also holds for g.

While it is often convenient to work "by induction" on pregames, in some situations this becomes awkward, so we also define accessor functions SetTheory.PGame.LeftMoves, SetTheory.PGame.RightMoves, SetTheory.PGame.moveLeft and SetTheory.PGame.moveRight. There is a relation PGame.Subsequent p q, saying that p can be reached by playing some non-empty sequence of moves starting from q, an instance WellFounded Subsequent, and a local tactic pgame_wf_tac which is helpful for discharging proof obligations in inductive proofs relying on this relation.

Order properties #

Pregames have both a and a < relation, satisfying the usual properties of a Preorder. The relation 0 < x means that x can always be won by Left, while 0 ≤ x means that x can be won by Left as the second player.

It turns out to be quite convenient to define various relations on top of these. We define the "less or fuzzy" relation x ⧏ y as ¬ y ≤ x, the equivalence relation x ≈ y as x ≤ y ∧ y ≤ x, and the fuzzy relation x ‖ y as x ⧏ y ∧ y ⧏ x. If 0 ⧏ x, then x can be won by Left as the first player. If x ≈ 0, then x can be won by the second player. If x ‖ 0, then x can be won by the first player.

Statements like zero_le_lf, zero_lf_le, etc. unfold these definitions. The theorems le_def and lf_def give a recursive characterisation of each relation in terms of themselves two moves later. The theorems zero_le, zero_lf, etc. also take into account that 0 has no moves.

Later, games will be defined as the quotient by the relation; that is to say, the Antisymmetrization of SetTheory.PGame.

Algebraic structures #

We next turn to defining the operations necessary to make games into a commutative additive group. Addition is defined for $x = \{xL | xR\}$ and $y = \{yL | yR\}$ by $x + y = \{xL + y, x + yL | xR + y, x + yR\}$. Negation is defined by $\{xL | xR\} = \{-xR | -xL\}$.

The order structures interact in the expected way with addition, so we have

theorem le_iff_sub_nonneg {x y : PGame} : x ≤ y ↔ 0 ≤ y - x := sorry
theorem lt_iff_sub_pos {x y : PGame} : x < y ↔ 0 < y - x := sorry

We show that these operations respect the equivalence relation, and hence descend to games. At the level of games, these operations satisfy all the laws of a commutative group. To prove the necessary equivalence relations at the level of pregames, we introduce the notion of a Relabelling of a game, and show, for example, that there is a relabelling between x + (y + z) and (x + y) + z.

Future work #

References #

The material here is all drawn from

An interested reader may like to formalise some of the material from

Pre-game moves #

inductive SetTheory.PGame :
Type (u + 1)

The type of pre-games, before we have quotiented by equivalence (PGame.Setoid). In ZFC, a combinatorial game is constructed from two sets of combinatorial games that have been constructed at an earlier stage. To do this in type theory, we say that a pre-game is built inductively from two families of pre-games indexed over any type in Type u. The resulting type PGame.{u} lives in Type (u+1), reflecting that it is a proper class in ZFC.

Instances For

    The indexing type for allowable moves by Left.

    Equations
    Instances For

      The indexing type for allowable moves by Right.

      Equations
      Instances For

        The new game after Left makes an allowed move.

        Equations
        Instances For

          The new game after Right makes an allowed move.

          Equations
          Instances For
            @[simp]
            theorem SetTheory.PGame.leftMoves_mk {xl : Type u_1} {xr : Type u_1} {xL : xlSetTheory.PGame} {xR : xrSetTheory.PGame} :
            (SetTheory.PGame.mk xl xr xL xR).LeftMoves = xl
            @[simp]
            theorem SetTheory.PGame.moveLeft_mk {xl : Type u_1} {xr : Type u_1} {xL : xlSetTheory.PGame} {xR : xrSetTheory.PGame} :
            (SetTheory.PGame.mk xl xr xL xR).moveLeft = xL
            @[simp]
            theorem SetTheory.PGame.rightMoves_mk {xl : Type u_1} {xr : Type u_1} {xL : xlSetTheory.PGame} {xR : xrSetTheory.PGame} :
            (SetTheory.PGame.mk xl xr xL xR).RightMoves = xr
            @[simp]
            theorem SetTheory.PGame.moveRight_mk {xl : Type u_1} {xr : Type u_1} {xL : xlSetTheory.PGame} {xR : xrSetTheory.PGame} :
            (SetTheory.PGame.mk xl xr xL xR).moveRight = xR

            Construct a pre-game from list of pre-games describing the available moves for Left and Right.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Converts a number into a left move for ofLists.

              Equations
              • SetTheory.PGame.toOfListsLeftMoves = ((Equiv.cast ).trans Equiv.ulift).symm
              Instances For

                Converts a number into a right move for ofLists.

                Equations
                • SetTheory.PGame.toOfListsRightMoves = ((Equiv.cast ).trans Equiv.ulift).symm
                Instances For
                  theorem SetTheory.PGame.ofLists_moveLeft {L : List SetTheory.PGame} {R : List SetTheory.PGame} (i : Fin L.length) :
                  (SetTheory.PGame.ofLists L R).moveLeft (SetTheory.PGame.toOfListsLeftMoves i) = L.get i
                  @[simp]
                  theorem SetTheory.PGame.ofLists_moveLeft' {L : List SetTheory.PGame} {R : List SetTheory.PGame} (i : (SetTheory.PGame.ofLists L R).LeftMoves) :
                  (SetTheory.PGame.ofLists L R).moveLeft i = L.get (SetTheory.PGame.toOfListsLeftMoves.symm i)
                  theorem SetTheory.PGame.ofLists_moveRight {L : List SetTheory.PGame} {R : List SetTheory.PGame} (i : Fin R.length) :
                  (SetTheory.PGame.ofLists L R).moveRight (SetTheory.PGame.toOfListsRightMoves i) = R.get i
                  @[simp]
                  theorem SetTheory.PGame.ofLists_moveRight' {L : List SetTheory.PGame} {R : List SetTheory.PGame} (i : (SetTheory.PGame.ofLists L R).RightMoves) :
                  (SetTheory.PGame.ofLists L R).moveRight i = R.get (SetTheory.PGame.toOfListsRightMoves.symm i)
                  def SetTheory.PGame.moveRecOn {C : SetTheory.PGameSort u_1} (x : SetTheory.PGame) (IH : (y : SetTheory.PGame) → ((i : y.LeftMoves) → C (y.moveLeft i))((j : y.RightMoves) → C (y.moveRight j))C y) :
                  C x

                  A variant of PGame.recOn expressed in terms of PGame.moveLeft and PGame.moveRight.

                  Both this and PGame.recOn describe Conway induction on games.

                  Equations
                  Instances For
                    theorem SetTheory.PGame.isOption_iff :
                    ∀ (a a_1 : SetTheory.PGame), a.IsOption a_1 (∃ (i : a_1.LeftMoves), a = a_1.moveLeft i) ∃ (i : a_1.RightMoves), a = a_1.moveRight i

                    IsOption x y means that x is either a left or right option for y.

                    • moveLeft: ∀ {x : SetTheory.PGame} (i : x.LeftMoves), (x.moveLeft i).IsOption x
                    • moveRight: ∀ {x : SetTheory.PGame} (i : x.RightMoves), (x.moveRight i).IsOption x
                    Instances For
                      theorem SetTheory.PGame.IsOption.mk_left {xl : Type u} {xr : Type u} (xL : xlSetTheory.PGame) (xR : xrSetTheory.PGame) (i : xl) :
                      (xL i).IsOption (SetTheory.PGame.mk xl xr xL xR)
                      theorem SetTheory.PGame.IsOption.mk_right {xl : Type u} {xr : Type u} (xL : xlSetTheory.PGame) (xR : xrSetTheory.PGame) (i : xr) :
                      (xR i).IsOption (SetTheory.PGame.mk xl xr xL xR)

                      Subsequent x y says that x can be obtained by playing some nonempty sequence of moves from y. It is the transitive closure of IsOption.

                      Equations
                      Instances For
                        theorem SetTheory.PGame.Subsequent.trans {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} :
                        x.Subsequent yy.Subsequent zx.Subsequent z
                        @[simp]
                        theorem SetTheory.PGame.Subsequent.moveLeft {x : SetTheory.PGame} (i : x.LeftMoves) :
                        (x.moveLeft i).Subsequent x
                        @[simp]
                        theorem SetTheory.PGame.Subsequent.moveRight {x : SetTheory.PGame} (j : x.RightMoves) :
                        (x.moveRight j).Subsequent x
                        @[simp]
                        theorem SetTheory.PGame.Subsequent.mk_left {xl : Type u_1} {xr : Type u_1} (xL : xlSetTheory.PGame) (xR : xrSetTheory.PGame) (i : xl) :
                        (xL i).Subsequent (SetTheory.PGame.mk xl xr xL xR)
                        @[simp]
                        theorem SetTheory.PGame.Subsequent.mk_right {xl : Type u_1} {xr : Type u_1} (xL : xlSetTheory.PGame) (xR : xrSetTheory.PGame) (j : xr) :
                        (xR j).Subsequent (SetTheory.PGame.mk xl xr xL xR)

                        Discharges proof obligations of the form Subsequent .. arising in termination proofs of definitions using well-founded recursion on PGame.

                        Equations
                        Instances For
                          @[simp]
                          theorem SetTheory.PGame.Subsequent.mk_right' {xl : Type u} {xr : Type u} (xL : xlSetTheory.PGame) (xR : xrSetTheory.PGame) (j : (SetTheory.PGame.mk xl xr xL xR).RightMoves) :
                          (xR j).Subsequent (SetTheory.PGame.mk xl xr xL xR)
                          @[simp]
                          theorem SetTheory.PGame.Subsequent.moveRight_mk_left {xl : Type u} {xr : Type u} {xR : xrSetTheory.PGame} {i : xl} (xL : xlSetTheory.PGame) (j : (xL i).RightMoves) :
                          ((xL i).moveRight j).Subsequent (SetTheory.PGame.mk xl xr xL xR)
                          @[simp]
                          theorem SetTheory.PGame.Subsequent.moveRight_mk_right {xl : Type u} {xr : Type u} {xL : xlSetTheory.PGame} {i : xr} (xR : xrSetTheory.PGame) (j : (xR i).RightMoves) :
                          ((xR i).moveRight j).Subsequent (SetTheory.PGame.mk xl xr xL xR)
                          @[simp]
                          theorem SetTheory.PGame.Subsequent.moveLeft_mk_left {xl : Type u} {xr : Type u} {xR : xrSetTheory.PGame} {i : xl} (xL : xlSetTheory.PGame) (j : (xL i).LeftMoves) :
                          ((xL i).moveLeft j).Subsequent (SetTheory.PGame.mk xl xr xL xR)
                          @[simp]
                          theorem SetTheory.PGame.Subsequent.moveLeft_mk_right {xl : Type u} {xr : Type u} {xL : xlSetTheory.PGame} {i : xr} (xR : xrSetTheory.PGame) (j : (xR i).LeftMoves) :
                          ((xR i).moveLeft j).Subsequent (SetTheory.PGame.mk xl xr xL xR)

                          Basic pre-games #

                          The pre-game Zero is defined by 0 = { | }.

                          Equations

                          The pre-game One is defined by 1 = { 0 | }.

                          Equations

                          Pre-game order relations #

                          The less or equal relation on pre-games.

                          If 0 ≤ x, then Left can win x as the second player.

                          Equations
                          • One or more equations did not get rendered due to their size.

                          The less or fuzzy relation on pre-games.

                          If 0 ⧏ x, then Left can win x as the first player.

                          Equations
                          Instances For

                            The less or fuzzy relation on pre-games.

                            If 0 ⧏ x, then Left can win x as the first player.

                            Equations
                            Instances For
                              @[simp]
                              @[simp]
                              theorem LE.le.not_gf {x : SetTheory.PGame} {y : SetTheory.PGame} :
                              x y¬y.LF x
                              theorem SetTheory.PGame.le_iff_forall_lf {x : SetTheory.PGame} {y : SetTheory.PGame} :
                              x y (∀ (i : x.LeftMoves), (x.moveLeft i).LF y) ∀ (j : y.RightMoves), x.LF (y.moveRight j)

                              Definition of x ≤ y on pre-games, in terms of .

                              The ordering here is chosen so that And.left refer to moves by Left, and And.right refer to moves by Right.

                              @[simp]
                              theorem SetTheory.PGame.mk_le_mk {xl : Type u_1} {xr : Type u_1} {xL : xlSetTheory.PGame} {xR : xrSetTheory.PGame} {yl : Type u_1} {yr : Type u_1} {yL : ylSetTheory.PGame} {yR : yrSetTheory.PGame} :
                              SetTheory.PGame.mk xl xr xL xR SetTheory.PGame.mk yl yr yL yR (∀ (i : xl), (xL i).LF (SetTheory.PGame.mk yl yr yL yR)) ∀ (j : yr), (SetTheory.PGame.mk xl xr xL xR).LF (yR j)

                              Definition of x ≤ y on pre-games built using the constructor.

                              theorem SetTheory.PGame.le_of_forall_lf {x : SetTheory.PGame} {y : SetTheory.PGame} (h₁ : ∀ (i : x.LeftMoves), (x.moveLeft i).LF y) (h₂ : ∀ (j : y.RightMoves), x.LF (y.moveRight j)) :
                              x y
                              theorem SetTheory.PGame.lf_iff_exists_le {x : SetTheory.PGame} {y : SetTheory.PGame} :
                              x.LF y (∃ (i : y.LeftMoves), x y.moveLeft i) ∃ (j : x.RightMoves), x.moveRight j y

                              Definition of x ⧏ y on pre-games, in terms of .

                              The ordering here is chosen so that or.inl refer to moves by Left, and or.inr refer to moves by Right.

                              @[simp]
                              theorem SetTheory.PGame.mk_lf_mk {xl : Type u_1} {xr : Type u_1} {xL : xlSetTheory.PGame} {xR : xrSetTheory.PGame} {yl : Type u_1} {yr : Type u_1} {yL : ylSetTheory.PGame} {yR : yrSetTheory.PGame} :
                              (SetTheory.PGame.mk xl xr xL xR).LF (SetTheory.PGame.mk yl yr yL yR) (∃ (i : yl), SetTheory.PGame.mk xl xr xL xR yL i) ∃ (j : xr), xR j SetTheory.PGame.mk yl yr yL yR

                              Definition of x ⧏ y on pre-games built using the constructor.

                              theorem SetTheory.PGame.moveLeft_lf_of_le {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x y) (i : x.LeftMoves) :
                              (x.moveLeft i).LF y
                              theorem LE.le.moveLeft_lf {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x y) (i : x.LeftMoves) :
                              (x.moveLeft i).LF y

                              Alias of SetTheory.PGame.moveLeft_lf_of_le.

                              theorem SetTheory.PGame.lf_moveRight_of_le {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x y) (j : y.RightMoves) :
                              x.LF (y.moveRight j)
                              theorem LE.le.lf_moveRight {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x y) (j : y.RightMoves) :
                              x.LF (y.moveRight j)

                              Alias of SetTheory.PGame.lf_moveRight_of_le.

                              theorem SetTheory.PGame.lf_of_moveRight_le {x : SetTheory.PGame} {y : SetTheory.PGame} {j : x.RightMoves} (h : x.moveRight j y) :
                              x.LF y
                              theorem SetTheory.PGame.lf_of_le_moveLeft {x : SetTheory.PGame} {y : SetTheory.PGame} {i : y.LeftMoves} (h : x y.moveLeft i) :
                              x.LF y
                              theorem SetTheory.PGame.lf_of_le_mk {xl : Type u_1} {xr : Type u_1} {xL : xlSetTheory.PGame} {xR : xrSetTheory.PGame} {y : SetTheory.PGame} :
                              SetTheory.PGame.mk xl xr xL xR y∀ (i : xl), (xL i).LF y
                              theorem SetTheory.PGame.lf_of_mk_le {x : SetTheory.PGame} {yl : Type u_1} {yr : Type u_1} {yL : ylSetTheory.PGame} {yR : yrSetTheory.PGame} :
                              x SetTheory.PGame.mk yl yr yL yR∀ (j : yr), x.LF (yR j)
                              theorem SetTheory.PGame.mk_lf_of_le {xl : Type u_1} {xr : Type u_1} {y : SetTheory.PGame} {j : xr} (xL : xlSetTheory.PGame) {xR : xrSetTheory.PGame} :
                              xR j y(SetTheory.PGame.mk xl xr xL xR).LF y
                              theorem SetTheory.PGame.lf_mk_of_le {x : SetTheory.PGame} {yl : Type u_1} {yr : Type u_1} {yL : ylSetTheory.PGame} (yR : yrSetTheory.PGame) {i : yl} :
                              x yL ix.LF (SetTheory.PGame.mk yl yr yL yR)
                              theorem SetTheory.PGame.lt_of_le_of_lf {x : SetTheory.PGame} {y : SetTheory.PGame} (h₁ : x y) (h₂ : x.LF y) :
                              x < y
                              theorem SetTheory.PGame.lf_of_lt {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x < y) :
                              x.LF y
                              theorem LT.lt.lf {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x < y) :
                              x.LF y

                              Alias of SetTheory.PGame.lf_of_lt.

                              theorem SetTheory.PGame.lf_of_le_of_lf {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x y) (h₂ : y.LF z) :
                              x.LF z
                              instance SetTheory.PGame.instTransLeLF :
                              Trans (fun (x x_1 : SetTheory.PGame) => x x_1) (fun (x x_1 : SetTheory.PGame) => x.LF x_1) fun (x x_1 : SetTheory.PGame) => x.LF x_1
                              Equations
                              theorem SetTheory.PGame.lf_of_lf_of_le {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x.LF y) (h₂ : y z) :
                              x.LF z
                              instance SetTheory.PGame.instTransLFLe :
                              Trans (fun (x x_1 : SetTheory.PGame) => x.LF x_1) (fun (x x_1 : SetTheory.PGame) => x x_1) fun (x x_1 : SetTheory.PGame) => x.LF x_1
                              Equations
                              theorem LE.le.trans_lf {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x y) (h₂ : y.LF z) :
                              x.LF z

                              Alias of SetTheory.PGame.lf_of_le_of_lf.

                              theorem SetTheory.PGame.LF.trans_le {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x.LF y) (h₂ : y z) :
                              x.LF z

                              Alias of SetTheory.PGame.lf_of_lf_of_le.

                              theorem SetTheory.PGame.lf_of_lt_of_lf {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x < y) (h₂ : y.LF z) :
                              x.LF z
                              theorem SetTheory.PGame.lf_of_lf_of_lt {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x.LF y) (h₂ : y < z) :
                              x.LF z
                              theorem LT.lt.trans_lf {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x < y) (h₂ : y.LF z) :
                              x.LF z

                              Alias of SetTheory.PGame.lf_of_lt_of_lf.

                              theorem SetTheory.PGame.LF.trans_lt {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x.LF y) (h₂ : y < z) :
                              x.LF z

                              Alias of SetTheory.PGame.lf_of_lf_of_lt.

                              theorem SetTheory.PGame.moveLeft_lf {x : SetTheory.PGame} (i : x.LeftMoves) :
                              (x.moveLeft i).LF x
                              theorem SetTheory.PGame.lf_moveRight {x : SetTheory.PGame} (j : x.RightMoves) :
                              x.LF (x.moveRight j)
                              theorem SetTheory.PGame.lf_mk {xl : Type u_1} {xr : Type u_1} (xL : xlSetTheory.PGame) (xR : xrSetTheory.PGame) (i : xl) :
                              (xL i).LF (SetTheory.PGame.mk xl xr xL xR)
                              theorem SetTheory.PGame.mk_lf {xl : Type u_1} {xr : Type u_1} (xL : xlSetTheory.PGame) (xR : xrSetTheory.PGame) (j : xr) :
                              (SetTheory.PGame.mk xl xr xL xR).LF (xR j)
                              theorem SetTheory.PGame.le_of_forall_lt {x : SetTheory.PGame} {y : SetTheory.PGame} (h₁ : ∀ (i : x.LeftMoves), x.moveLeft i < y) (h₂ : ∀ (j : y.RightMoves), x < y.moveRight j) :
                              x y

                              This special case of PGame.le_of_forall_lf is useful when dealing with surreals, where < is preferred over .

                              theorem SetTheory.PGame.le_def {x : SetTheory.PGame} {y : SetTheory.PGame} :
                              x y (∀ (i : x.LeftMoves), (∃ (i' : y.LeftMoves), x.moveLeft i y.moveLeft i') ∃ (j : (x.moveLeft i).RightMoves), (x.moveLeft i).moveRight j y) ∀ (j : y.RightMoves), (∃ (i : (y.moveRight j).LeftMoves), x (y.moveRight j).moveLeft i) ∃ (j' : x.RightMoves), x.moveRight j' y.moveRight j

                              The definition of x ≤ y on pre-games, in terms of two moves later.

                              theorem SetTheory.PGame.lf_def {x : SetTheory.PGame} {y : SetTheory.PGame} :
                              x.LF y (∃ (i : y.LeftMoves), (∀ (i' : x.LeftMoves), (x.moveLeft i').LF (y.moveLeft i)) ∀ (j : (y.moveLeft i).RightMoves), x.LF ((y.moveLeft i).moveRight j)) ∃ (j : x.RightMoves), (∀ (i : (x.moveRight j).LeftMoves), ((x.moveRight j).moveLeft i).LF y) ∀ (j' : y.RightMoves), (x.moveRight j).LF (y.moveRight j')

                              The definition of x ⧏ y on pre-games, in terms of two moves later.

                              theorem SetTheory.PGame.zero_le_lf {x : SetTheory.PGame} :
                              0 x ∀ (j : x.RightMoves), SetTheory.PGame.LF 0 (x.moveRight j)

                              The definition of 0 ≤ x on pre-games, in terms of 0 ⧏.

                              theorem SetTheory.PGame.le_zero_lf {x : SetTheory.PGame} :
                              x 0 ∀ (i : x.LeftMoves), (x.moveLeft i).LF 0

                              The definition of x ≤ 0 on pre-games, in terms of ⧏ 0.

                              theorem SetTheory.PGame.zero_lf_le {x : SetTheory.PGame} :
                              SetTheory.PGame.LF 0 x ∃ (i : x.LeftMoves), 0 x.moveLeft i

                              The definition of 0 ⧏ x on pre-games, in terms of 0 ≤.

                              theorem SetTheory.PGame.lf_zero_le {x : SetTheory.PGame} :
                              x.LF 0 ∃ (j : x.RightMoves), x.moveRight j 0

                              The definition of x ⧏ 0 on pre-games, in terms of ≤ 0.

                              theorem SetTheory.PGame.zero_le {x : SetTheory.PGame} :
                              0 x ∀ (j : x.RightMoves), ∃ (i : (x.moveRight j).LeftMoves), 0 (x.moveRight j).moveLeft i

                              The definition of 0 ≤ x on pre-games, in terms of 0 ≤ two moves later.

                              theorem SetTheory.PGame.le_zero {x : SetTheory.PGame} :
                              x 0 ∀ (i : x.LeftMoves), ∃ (j : (x.moveLeft i).RightMoves), (x.moveLeft i).moveRight j 0

                              The definition of x ≤ 0 on pre-games, in terms of ≤ 0 two moves later.

                              theorem SetTheory.PGame.zero_lf {x : SetTheory.PGame} :
                              SetTheory.PGame.LF 0 x ∃ (i : x.LeftMoves), ∀ (j : (x.moveLeft i).RightMoves), SetTheory.PGame.LF 0 ((x.moveLeft i).moveRight j)

                              The definition of 0 ⧏ x on pre-games, in terms of 0 ⧏ two moves later.

                              theorem SetTheory.PGame.lf_zero {x : SetTheory.PGame} :
                              x.LF 0 ∃ (j : x.RightMoves), ∀ (i : (x.moveRight j).LeftMoves), ((x.moveRight j).moveLeft i).LF 0

                              The definition of x ⧏ 0 on pre-games, in terms of ⧏ 0 two moves later.

                              noncomputable def SetTheory.PGame.rightResponse {x : SetTheory.PGame} (h : x 0) (i : x.LeftMoves) :
                              (x.moveLeft i).RightMoves

                              Given a game won by the right player when they play second, provide a response to any move by left.

                              Equations
                              Instances For
                                theorem SetTheory.PGame.rightResponse_spec {x : SetTheory.PGame} (h : x 0) (i : x.LeftMoves) :
                                (x.moveLeft i).moveRight (SetTheory.PGame.rightResponse h i) 0

                                Show that the response for right provided by rightResponse preserves the right-player-wins condition.

                                noncomputable def SetTheory.PGame.leftResponse {x : SetTheory.PGame} (h : 0 x) (j : x.RightMoves) :
                                (x.moveRight j).LeftMoves

                                Given a game won by the left player when they play second, provide a response to any move by right.

                                Equations
                                Instances For
                                  theorem SetTheory.PGame.leftResponse_spec {x : SetTheory.PGame} (h : 0 x) (j : x.RightMoves) :
                                  0 (x.moveRight j).moveLeft (SetTheory.PGame.leftResponse h j)

                                  Show that the response for left provided by leftResponse preserves the left-player-wins condition.

                                  A small family of pre-games is bounded above.

                                  A small set of pre-games is bounded above.

                                  A small family of pre-games is bounded below.

                                  A small set of pre-games is bounded below.

                                  The equivalence relation on pre-games. Two pre-games x, y are equivalent if x ≤ y and y ≤ x.

                                  If x ≈ 0, then the second player can always win x.

                                  Equations
                                  Instances For
                                    theorem SetTheory.PGame.le_of_le_of_equiv {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x y) (h₂ : y z) :
                                    x z
                                    instance SetTheory.PGame.instTransLeEquiv :
                                    Trans (fun (x x_1 : SetTheory.PGame) => x x_1) (fun (x x_1 : SetTheory.PGame) => x x_1) fun (x x_1 : SetTheory.PGame) => x x_1
                                    Equations
                                    instance SetTheory.PGame.instTransEquivLe :
                                    Trans (fun (x x_1 : SetTheory.PGame) => x x_1) (fun (x x_1 : SetTheory.PGame) => x x_1) fun (x x_1 : SetTheory.PGame) => x x_1
                                    Equations
                                    theorem SetTheory.PGame.le_congr_imp {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) (h : x₁ y₁) :
                                    x₂ y₂
                                    theorem SetTheory.PGame.le_congr {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) :
                                    x₁ y₁ x₂ y₂
                                    theorem SetTheory.PGame.le_congr_left {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y : SetTheory.PGame} (hx : x₁ x₂) :
                                    x₁ y x₂ y
                                    theorem SetTheory.PGame.le_congr_right {x : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hy : y₁ y₂) :
                                    x y₁ x y₂
                                    theorem SetTheory.PGame.lf_congr {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) :
                                    x₁.LF y₁ x₂.LF y₂
                                    theorem SetTheory.PGame.lf_congr_imp {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) :
                                    x₁.LF y₁x₂.LF y₂
                                    theorem SetTheory.PGame.lf_congr_left {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y : SetTheory.PGame} (hx : x₁ x₂) :
                                    x₁.LF y x₂.LF y
                                    theorem SetTheory.PGame.lf_congr_right {x : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hy : y₁ y₂) :
                                    x.LF y₁ x.LF y₂
                                    theorem SetTheory.PGame.lf_of_lf_of_equiv {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x.LF y) (h₂ : y z) :
                                    x.LF z
                                    instance SetTheory.PGame.instTransLFEquiv :
                                    Trans (fun (x x_1 : SetTheory.PGame) => x.LF x_1) (fun (x x_1 : SetTheory.PGame) => x x_1) fun (x x_1 : SetTheory.PGame) => x.LF x_1
                                    Equations
                                    theorem SetTheory.PGame.lf_of_equiv_of_lf {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x y) :
                                    y.LF zx.LF z
                                    instance SetTheory.PGame.instTransEquivLF :
                                    Trans (fun (x x_1 : SetTheory.PGame) => x x_1) (fun (x x_1 : SetTheory.PGame) => x.LF x_1) fun (x x_1 : SetTheory.PGame) => x.LF x_1
                                    Equations
                                    theorem SetTheory.PGame.lt_of_lt_of_equiv {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x < y) (h₂ : y z) :
                                    x < z
                                    instance SetTheory.PGame.instTransLtEquiv :
                                    Trans (fun (x x_1 : SetTheory.PGame) => x < x_1) (fun (x x_1 : SetTheory.PGame) => x x_1) fun (x x_1 : SetTheory.PGame) => x < x_1
                                    Equations
                                    instance SetTheory.PGame.instTransEquivLt :
                                    Trans (fun (x x_1 : SetTheory.PGame) => x x_1) (fun (x x_1 : SetTheory.PGame) => x < x_1) fun (x x_1 : SetTheory.PGame) => x < x_1
                                    Equations
                                    theorem SetTheory.PGame.lt_congr_imp {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) (h : x₁ < y₁) :
                                    x₂ < y₂
                                    theorem SetTheory.PGame.lt_congr {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) :
                                    x₁ < y₁ x₂ < y₂
                                    theorem SetTheory.PGame.lt_congr_left {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y : SetTheory.PGame} (hx : x₁ x₂) :
                                    x₁ < y x₂ < y
                                    theorem SetTheory.PGame.lt_congr_right {x : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hy : y₁ y₂) :
                                    x < y₁ x < y₂
                                    theorem SetTheory.PGame.equiv_congr_left {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} :
                                    y₁ y₂ ∀ (x₁ : SetTheory.PGame), x₁ y₁ x₁ y₂
                                    theorem SetTheory.PGame.equiv_congr_right {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} :
                                    x₁ x₂ ∀ (y₁ : SetTheory.PGame), x₁ y₁ x₂ y₁
                                    theorem SetTheory.PGame.equiv_of_mk_equiv {x : SetTheory.PGame} {y : SetTheory.PGame} (L : x.LeftMoves y.LeftMoves) (R : x.RightMoves y.RightMoves) (hl : ∀ (i : x.LeftMoves), x.moveLeft i y.moveLeft (L i)) (hr : ∀ (j : x.RightMoves), x.moveRight j y.moveRight (R j)) :
                                    x y

                                    The fuzzy, confused, or incomparable relation on pre-games.

                                    If x ‖ 0, then the first player can always win x.

                                    Equations
                                    • x.Fuzzy y = (x.LF y y.LF x)
                                    Instances For

                                      The fuzzy, confused, or incomparable relation on pre-games.

                                      If x ‖ 0, then the first player can always win x.

                                      Equations
                                      Instances For
                                        theorem SetTheory.PGame.Fuzzy.swap {x : SetTheory.PGame} {y : SetTheory.PGame} :
                                        x.Fuzzy yy.Fuzzy x
                                        theorem SetTheory.PGame.lf_of_fuzzy {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x.Fuzzy y) :
                                        x.LF y
                                        theorem SetTheory.PGame.lt_or_fuzzy_of_lf {x : SetTheory.PGame} {y : SetTheory.PGame} :
                                        x.LF yx < y x.Fuzzy y
                                        theorem SetTheory.PGame.fuzzy_congr {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) :
                                        x₁.Fuzzy y₁ x₂.Fuzzy y₂
                                        theorem SetTheory.PGame.fuzzy_congr_imp {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x₁ x₂) (hy : y₁ y₂) :
                                        x₁.Fuzzy y₁x₂.Fuzzy y₂
                                        theorem SetTheory.PGame.fuzzy_congr_left {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y : SetTheory.PGame} (hx : x₁ x₂) :
                                        x₁.Fuzzy y x₂.Fuzzy y
                                        theorem SetTheory.PGame.fuzzy_congr_right {x : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hy : y₁ y₂) :
                                        x.Fuzzy y₁ x.Fuzzy y₂
                                        theorem SetTheory.PGame.fuzzy_of_fuzzy_of_equiv {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x.Fuzzy y) (h₂ : y z) :
                                        x.Fuzzy z
                                        theorem SetTheory.PGame.fuzzy_of_equiv_of_fuzzy {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : x y) (h₂ : y.Fuzzy z) :
                                        x.Fuzzy z

                                        Exactly one of the following is true (although we don't prove this here).

                                        Relabellings #

                                        Relabelling x y says that x and y are really the same game, just dressed up differently. Specifically, there is a bijection between the moves for Left in x and in y, and similarly for Right, and under these bijections we inductively have Relabellings for the consequent games.

                                        • mk: {x y : SetTheory.PGame} → (L : x.LeftMoves y.LeftMoves) → (R : x.RightMoves y.RightMoves) → ((i : x.LeftMoves) → (x.moveLeft i).Relabelling (y.moveLeft (L i)))((j : x.RightMoves) → (x.moveRight j).Relabelling (y.moveRight (R j)))x.Relabelling y
                                        Instances For

                                          Relabelling x y says that x and y are really the same game, just dressed up differently. Specifically, there is a bijection between the moves for Left in x and in y, and similarly for Right, and under these bijections we inductively have Relabellings for the consequent games.

                                          Equations
                                          Instances For
                                            def SetTheory.PGame.Relabelling.mk' {x : SetTheory.PGame} {y : SetTheory.PGame} (L : y.LeftMoves x.LeftMoves) (R : y.RightMoves x.RightMoves) (hL : (i : y.LeftMoves) → (x.moveLeft (L i)).Relabelling (y.moveLeft i)) (hR : (j : y.RightMoves) → (x.moveRight (R j)).Relabelling (y.moveRight j)) :
                                            x.Relabelling y

                                            A constructor for relabellings swapping the equivalences.

                                            Equations
                                            Instances For
                                              def SetTheory.PGame.Relabelling.leftMovesEquiv {x : SetTheory.PGame} {y : SetTheory.PGame} :
                                              x.Relabelling yx.LeftMoves y.LeftMoves

                                              The equivalence between left moves of x and y given by the relabelling.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem SetTheory.PGame.Relabelling.mk_leftMovesEquiv {x : SetTheory.PGame} {y : SetTheory.PGame} {L : x.LeftMoves y.LeftMoves} {R : x.RightMoves y.RightMoves} {hL : (i : x.LeftMoves) → (x.moveLeft i).Relabelling (y.moveLeft (L i))} {hR : (j : x.RightMoves) → (x.moveRight j).Relabelling (y.moveRight (R j))} :
                                                (SetTheory.PGame.Relabelling.mk L R hL hR).leftMovesEquiv = L
                                                @[simp]
                                                theorem SetTheory.PGame.Relabelling.mk'_leftMovesEquiv {x : SetTheory.PGame} {y : SetTheory.PGame} {L : y.LeftMoves x.LeftMoves} {R : y.RightMoves x.RightMoves} {hL : (i : y.LeftMoves) → (x.moveLeft (L i)).Relabelling (y.moveLeft i)} {hR : (j : y.RightMoves) → (x.moveRight (R j)).Relabelling (y.moveRight j)} :
                                                (SetTheory.PGame.Relabelling.mk' L R hL hR).leftMovesEquiv = L.symm
                                                def SetTheory.PGame.Relabelling.rightMovesEquiv {x : SetTheory.PGame} {y : SetTheory.PGame} :
                                                x.Relabelling yx.RightMoves y.RightMoves

                                                The equivalence between right moves of x and y given by the relabelling.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem SetTheory.PGame.Relabelling.mk_rightMovesEquiv {x : SetTheory.PGame} {y : SetTheory.PGame} {L : x.LeftMoves y.LeftMoves} {R : x.RightMoves y.RightMoves} {hL : (i : x.LeftMoves) → (x.moveLeft i).Relabelling (y.moveLeft (L i))} {hR : (j : x.RightMoves) → (x.moveRight j).Relabelling (y.moveRight (R j))} :
                                                  (SetTheory.PGame.Relabelling.mk L R hL hR).rightMovesEquiv = R
                                                  @[simp]
                                                  theorem SetTheory.PGame.Relabelling.mk'_rightMovesEquiv {x : SetTheory.PGame} {y : SetTheory.PGame} {L : y.LeftMoves x.LeftMoves} {R : y.RightMoves x.RightMoves} {hL : (i : y.LeftMoves) → (x.moveLeft (L i)).Relabelling (y.moveLeft i)} {hR : (j : y.RightMoves) → (x.moveRight (R j)).Relabelling (y.moveRight j)} :
                                                  (SetTheory.PGame.Relabelling.mk' L R hL hR).rightMovesEquiv = R.symm
                                                  def SetTheory.PGame.Relabelling.moveLeft {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) (i : x.LeftMoves) :
                                                  (x.moveLeft i).Relabelling (y.moveLeft (r.leftMovesEquiv i))

                                                  A left move of x is a relabelling of a left move of y.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    def SetTheory.PGame.Relabelling.moveLeftSymm {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) (i : y.LeftMoves) :
                                                    (x.moveLeft (r.leftMovesEquiv.symm i)).Relabelling (y.moveLeft i)

                                                    A left move of y is a relabelling of a left move of x.

                                                    Equations
                                                    Instances For
                                                      def SetTheory.PGame.Relabelling.moveRight {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) (i : x.RightMoves) :
                                                      (x.moveRight i).Relabelling (y.moveRight (r.rightMovesEquiv i))

                                                      A right move of x is a relabelling of a right move of y.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        def SetTheory.PGame.Relabelling.moveRightSymm {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) (i : y.RightMoves) :
                                                        (x.moveRight (r.rightMovesEquiv.symm i)).Relabelling (y.moveRight i)

                                                        A right move of y is a relabelling of a right move of x.

                                                        Equations
                                                        Instances For
                                                          @[irreducible]

                                                          The identity relabelling.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            def SetTheory.PGame.Relabelling.symm {x : SetTheory.PGame} {y : SetTheory.PGame} :
                                                            x.Relabelling yy.Relabelling x

                                                            Flip a relabelling.

                                                            Equations
                                                            Instances For
                                                              @[irreducible]
                                                              theorem SetTheory.PGame.Relabelling.le {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) :
                                                              x y
                                                              theorem SetTheory.PGame.Relabelling.ge {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) :
                                                              y x
                                                              theorem SetTheory.PGame.Relabelling.equiv {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) :
                                                              x y

                                                              A relabelling lets us prove equivalence of games.

                                                              def SetTheory.PGame.Relabelling.trans {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} :
                                                              x.Relabelling yy.Relabelling zx.Relabelling z

                                                              Transitivity of relabelling.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                def SetTheory.PGame.Relabelling.isEmpty (x : SetTheory.PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] :
                                                                x.Relabelling 0

                                                                Any game without left or right moves is a relabelling of 0.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  theorem SetTheory.PGame.Equiv.isEmpty (x : SetTheory.PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] :
                                                                  x 0
                                                                  instance SetTheory.PGame.instCoeRelabellingEquiv {x : SetTheory.PGame} {y : SetTheory.PGame} :
                                                                  Coe (x.Relabelling y) (x y)
                                                                  Equations
                                                                  • SetTheory.PGame.instCoeRelabellingEquiv = { coe := }
                                                                  def SetTheory.PGame.relabel {x : SetTheory.PGame} {xl' : Type u_1} {xr' : Type u_1} (el : xl' x.LeftMoves) (er : xr' x.RightMoves) :

                                                                  Replace the types indexing the next moves for Left and Right by equivalent types.

                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem SetTheory.PGame.relabel_moveLeft' {x : SetTheory.PGame} {xl' : Type u_1} {xr' : Type u_1} (el : xl' x.LeftMoves) (er : xr' x.RightMoves) (i : xl') :
                                                                    (SetTheory.PGame.relabel el er).moveLeft i = x.moveLeft (el i)
                                                                    theorem SetTheory.PGame.relabel_moveLeft {x : SetTheory.PGame} {xl' : Type u_1} {xr' : Type u_1} (el : xl' x.LeftMoves) (er : xr' x.RightMoves) (i : x.LeftMoves) :
                                                                    (SetTheory.PGame.relabel el er).moveLeft (el.symm i) = x.moveLeft i
                                                                    @[simp]
                                                                    theorem SetTheory.PGame.relabel_moveRight' {x : SetTheory.PGame} {xl' : Type u_1} {xr' : Type u_1} (el : xl' x.LeftMoves) (er : xr' x.RightMoves) (j : xr') :
                                                                    (SetTheory.PGame.relabel el er).moveRight j = x.moveRight (er j)
                                                                    theorem SetTheory.PGame.relabel_moveRight {x : SetTheory.PGame} {xl' : Type u_1} {xr' : Type u_1} (el : xl' x.LeftMoves) (er : xr' x.RightMoves) (j : x.RightMoves) :
                                                                    (SetTheory.PGame.relabel el er).moveRight (er.symm j) = x.moveRight j
                                                                    def SetTheory.PGame.relabelRelabelling {x : SetTheory.PGame} {xl' : Type u_1} {xr' : Type u_1} (el : xl' x.LeftMoves) (er : xr' x.RightMoves) :
                                                                    x.Relabelling (SetTheory.PGame.relabel el er)

                                                                    The game obtained by relabelling the next moves is a relabelling of the original game.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For

                                                                      Negation #

                                                                      The negation of {L | R} is {-R | -L}.

                                                                      Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem SetTheory.PGame.neg_def {xl : Type u_1} {xr : Type u_1} {xL : xlSetTheory.PGame} {xR : xrSetTheory.PGame} :
                                                                        -SetTheory.PGame.mk xl xr xL xR = SetTheory.PGame.mk xr xl (fun (j : xr) => -xR j) fun (i : xl) => -xL i
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        theorem SetTheory.PGame.isOption_neg {x : SetTheory.PGame} {y : SetTheory.PGame} :
                                                                        x.IsOption (-y) (-x).IsOption y
                                                                        @[simp]
                                                                        theorem SetTheory.PGame.isOption_neg_neg {x : SetTheory.PGame} {y : SetTheory.PGame} :
                                                                        (-x).IsOption (-y) x.IsOption y
                                                                        theorem SetTheory.PGame.leftMoves_neg (x : SetTheory.PGame) :
                                                                        (-x).LeftMoves = x.RightMoves
                                                                        theorem SetTheory.PGame.rightMoves_neg (x : SetTheory.PGame) :
                                                                        (-x).RightMoves = x.LeftMoves
                                                                        def SetTheory.PGame.toLeftMovesNeg {x : SetTheory.PGame} :
                                                                        x.RightMoves (-x).LeftMoves

                                                                        Turns a right move for x into a left move for -x and vice versa.

                                                                        Even though these types are the same (not definitionally so), this is the preferred way to convert between them.

                                                                        Equations
                                                                        Instances For
                                                                          def SetTheory.PGame.toRightMovesNeg {x : SetTheory.PGame} :
                                                                          x.LeftMoves (-x).RightMoves

                                                                          Turns a left move for x into a right move for -x and vice versa.

                                                                          Even though these types are the same (not definitionally so), this is the preferred way to convert between them.

                                                                          Equations
                                                                          Instances For
                                                                            theorem SetTheory.PGame.moveLeft_neg {x : SetTheory.PGame} (i : x.RightMoves) :
                                                                            (-x).moveLeft (SetTheory.PGame.toLeftMovesNeg i) = -x.moveRight i
                                                                            @[simp]
                                                                            theorem SetTheory.PGame.moveLeft_neg' {x : SetTheory.PGame} (i : (-x).LeftMoves) :
                                                                            (-x).moveLeft i = -x.moveRight (SetTheory.PGame.toLeftMovesNeg.symm i)
                                                                            theorem SetTheory.PGame.moveRight_neg {x : SetTheory.PGame} (i : x.LeftMoves) :
                                                                            (-x).moveRight (SetTheory.PGame.toRightMovesNeg i) = -x.moveLeft i
                                                                            @[simp]
                                                                            theorem SetTheory.PGame.moveRight_neg' {x : SetTheory.PGame} (i : (-x).RightMoves) :
                                                                            (-x).moveRight i = -x.moveLeft (SetTheory.PGame.toRightMovesNeg.symm i)
                                                                            theorem SetTheory.PGame.moveLeft_neg_symm {x : SetTheory.PGame} (i : (-x).RightMoves) :
                                                                            x.moveLeft (SetTheory.PGame.toRightMovesNeg.symm i) = -(-x).moveRight i
                                                                            theorem SetTheory.PGame.moveLeft_neg_symm' {x : SetTheory.PGame} (i : x.LeftMoves) :
                                                                            x.moveLeft i = -(-x).moveRight (SetTheory.PGame.toRightMovesNeg i)
                                                                            theorem SetTheory.PGame.moveRight_neg_symm {x : SetTheory.PGame} (i : (-x).LeftMoves) :
                                                                            x.moveRight (SetTheory.PGame.toLeftMovesNeg.symm i) = -(-x).moveLeft i
                                                                            theorem SetTheory.PGame.moveRight_neg_symm' {x : SetTheory.PGame} (i : x.RightMoves) :
                                                                            x.moveRight i = -(-x).moveLeft (SetTheory.PGame.toLeftMovesNeg i)
                                                                            def SetTheory.PGame.Relabelling.negCongr {x : SetTheory.PGame} {y : SetTheory.PGame} :
                                                                            x.Relabelling y(-x).Relabelling (-y)

                                                                            If x has the same moves as y, then -x has the same moves as -y.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              @[simp]
                                                                              @[simp]
                                                                              theorem SetTheory.PGame.neg_fuzzy_neg_iff {x : SetTheory.PGame} {y : SetTheory.PGame} :
                                                                              (-x).Fuzzy (-y) x.Fuzzy y
                                                                              theorem SetTheory.PGame.neg_fuzzy_iff {x : SetTheory.PGame} {y : SetTheory.PGame} :
                                                                              (-x).Fuzzy y x.Fuzzy (-y)
                                                                              @[simp]
                                                                              theorem SetTheory.PGame.neg_fuzzy_zero_iff {x : SetTheory.PGame} :
                                                                              (-x).Fuzzy 0 x.Fuzzy 0

                                                                              Addition and subtraction #

                                                                              The sum of x = {xL | xR} and y = {yL | yR} is {xL + y, x + yL | xR + y, x + yR}.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.

                                                                              The pre-game ((0+1)+⋯)+1.

                                                                              Equations
                                                                              @[simp]
                                                                              theorem SetTheory.PGame.nat_succ (n : ) :
                                                                              (n + 1) = n + 1
                                                                              instance SetTheory.PGame.isEmpty_leftMoves_add (x : SetTheory.PGame) (y : SetTheory.PGame) [IsEmpty x.LeftMoves] [IsEmpty y.LeftMoves] :
                                                                              IsEmpty (x + y).LeftMoves
                                                                              Equations
                                                                              • =
                                                                              instance SetTheory.PGame.isEmpty_rightMoves_add (x : SetTheory.PGame) (y : SetTheory.PGame) [IsEmpty x.RightMoves] [IsEmpty y.RightMoves] :
                                                                              IsEmpty (x + y).RightMoves
                                                                              Equations
                                                                              • =
                                                                              @[irreducible]

                                                                              x + 0 has exactly the same moves as x.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For

                                                                                x + 0 is equivalent to x.

                                                                                0 + x has exactly the same moves as x.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For

                                                                                  0 + x is equivalent to x.

                                                                                  theorem SetTheory.PGame.leftMoves_add (x : SetTheory.PGame) (y : SetTheory.PGame) :
                                                                                  (x + y).LeftMoves = (x.LeftMoves y.LeftMoves)
                                                                                  theorem SetTheory.PGame.rightMoves_add (x : SetTheory.PGame) (y : SetTheory.PGame) :
                                                                                  (x + y).RightMoves = (x.RightMoves y.RightMoves)
                                                                                  def SetTheory.PGame.toLeftMovesAdd {x : SetTheory.PGame} {y : SetTheory.PGame} :
                                                                                  x.LeftMoves y.LeftMoves (x + y).LeftMoves

                                                                                  Converts a left move for x or y into a left move for x + y and vice versa.

                                                                                  Even though these types are the same (not definitionally so), this is the preferred way to convert between them.

                                                                                  Equations
                                                                                  Instances For
                                                                                    def SetTheory.PGame.toRightMovesAdd {x : SetTheory.PGame} {y : SetTheory.PGame} :
                                                                                    x.RightMoves y.RightMoves (x + y).RightMoves

                                                                                    Converts a right move for x or y into a right move for x + y and vice versa.

                                                                                    Even though these types are the same (not definitionally so), this is the preferred way to convert between them.

                                                                                    Equations
                                                                                    Instances For
                                                                                      @[simp]
                                                                                      theorem SetTheory.PGame.mk_add_moveLeft_inl {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : xlSetTheory.PGame} {xR : xrSetTheory.PGame} {yL : ylSetTheory.PGame} {yR : yrSetTheory.PGame} {i : xl} :
                                                                                      (SetTheory.PGame.mk xl xr xL xR + SetTheory.PGame.mk yl yr yL yR).moveLeft (Sum.inl i) = (SetTheory.PGame.mk xl xr xL xR).moveLeft i + SetTheory.PGame.mk yl yr yL yR
                                                                                      @[simp]
                                                                                      theorem SetTheory.PGame.add_moveLeft_inl {x : SetTheory.PGame} (y : SetTheory.PGame) (i : x.LeftMoves) :
                                                                                      (x + y).moveLeft (SetTheory.PGame.toLeftMovesAdd (Sum.inl i)) = x.moveLeft i + y
                                                                                      @[simp]
                                                                                      theorem SetTheory.PGame.mk_add_moveRight_inl {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : xlSetTheory.PGame} {xR : xrSetTheory.PGame} {yL : ylSetTheory.PGame} {yR : yrSetTheory.PGame} {i : xr} :
                                                                                      (SetTheory.PGame.mk xl xr xL xR + SetTheory.PGame.mk yl yr yL yR).moveRight (Sum.inl i) = (SetTheory.PGame.mk xl xr xL xR).moveRight i + SetTheory.PGame.mk yl yr yL yR
                                                                                      @[simp]
                                                                                      theorem SetTheory.PGame.add_moveRight_inl {x : SetTheory.PGame} (y : SetTheory.PGame) (i : x.RightMoves) :
                                                                                      (x + y).moveRight (SetTheory.PGame.toRightMovesAdd (Sum.inl i)) = x.moveRight i + y
                                                                                      @[simp]
                                                                                      theorem SetTheory.PGame.mk_add_moveLeft_inr {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : xlSetTheory.PGame} {xR : xrSetTheory.PGame} {yL : ylSetTheory.PGame} {yR : yrSetTheory.PGame} {i : yl} :
                                                                                      (SetTheory.PGame.mk xl xr xL xR + SetTheory.PGame.mk yl yr yL yR).moveLeft (Sum.inr i) = SetTheory.PGame.mk xl xr xL xR + (SetTheory.PGame.mk yl yr yL yR).moveLeft i
                                                                                      @[simp]
                                                                                      theorem SetTheory.PGame.add_moveLeft_inr (x : SetTheory.PGame) {y : SetTheory.PGame} (i : y.LeftMoves) :
                                                                                      (x + y).moveLeft (SetTheory.PGame.toLeftMovesAdd (Sum.inr i)) = x + y.moveLeft i
                                                                                      @[simp]
                                                                                      theorem SetTheory.PGame.mk_add_moveRight_inr {xl : Type u_1} {xr : Type u_1} {yl : Type u_1} {yr : Type u_1} {xL : xlSetTheory.PGame} {xR : xrSetTheory.PGame} {yL : ylSetTheory.PGame} {yR : yrSetTheory.PGame} {i : yr} :
                                                                                      (SetTheory.PGame.mk xl xr xL xR + SetTheory.PGame.mk yl yr yL yR).moveRight (Sum.inr i) = SetTheory.PGame.mk xl xr xL xR + (SetTheory.PGame.mk yl yr yL yR).moveRight i
                                                                                      @[simp]
                                                                                      theorem SetTheory.PGame.add_moveRight_inr (x : SetTheory.PGame) {y : SetTheory.PGame} (i : y.RightMoves) :
                                                                                      (x + y).moveRight (SetTheory.PGame.toRightMovesAdd (Sum.inr i)) = x + y.moveRight i
                                                                                      theorem SetTheory.PGame.leftMoves_add_cases {x : SetTheory.PGame} {y : SetTheory.PGame} (k : (x + y).LeftMoves) {P : (x + y).LeftMovesProp} (hl : ∀ (i : x.LeftMoves), P (SetTheory.PGame.toLeftMovesAdd (Sum.inl i))) (hr : ∀ (i : y.LeftMoves), P (SetTheory.PGame.toLeftMovesAdd (Sum.inr i))) :
                                                                                      P k
                                                                                      theorem SetTheory.PGame.rightMoves_add_cases {x : SetTheory.PGame} {y : SetTheory.PGame} (k : (x + y).RightMoves) {P : (x + y).RightMovesProp} (hl : ∀ (j : x.RightMoves), P (SetTheory.PGame.toRightMovesAdd (Sum.inl j))) (hr : ∀ (j : y.RightMoves), P (SetTheory.PGame.toRightMovesAdd (Sum.inr j))) :
                                                                                      P k
                                                                                      instance SetTheory.PGame.isEmpty_nat_rightMoves (n : ) :
                                                                                      IsEmpty (n).RightMoves
                                                                                      Equations
                                                                                      • =
                                                                                      @[irreducible]
                                                                                      def SetTheory.PGame.Relabelling.addCongr {w : SetTheory.PGame} {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} :
                                                                                      w.Relabelling xy.Relabelling z(w + y).Relabelling (x + z)

                                                                                      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.

                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        def SetTheory.PGame.Relabelling.subCongr {w : SetTheory.PGame} {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : w.Relabelling x) (h₂ : y.Relabelling z) :
                                                                                        (w - y).Relabelling (x - z)

                                                                                        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.

                                                                                        Equations
                                                                                        • h₁.subCongr h₂ = h₁.addCongr h₂.negCongr
                                                                                        Instances For
                                                                                          @[irreducible]
                                                                                          def SetTheory.PGame.negAddRelabelling (x : SetTheory.PGame) (y : SetTheory.PGame) :
                                                                                          (-(x + y)).Relabelling (-x + -y)

                                                                                          -(x + y) has exactly the same moves as -x + -y.

                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            @[irreducible]
                                                                                            def SetTheory.PGame.addCommRelabelling (x : SetTheory.PGame) (y : SetTheory.PGame) :
                                                                                            (x + y).Relabelling (y + x)

                                                                                            x + y has exactly the same moves as y + x.

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              @[irreducible]
                                                                                              def SetTheory.PGame.addAssocRelabelling (x : SetTheory.PGame) (y : SetTheory.PGame) (z : SetTheory.PGame) :
                                                                                              (x + y + z).Relabelling (x + (y + z))

                                                                                              (x + y) + z has exactly the same moves as x + (y + z).

                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For
                                                                                                theorem SetTheory.PGame.add_lf_add_right {y : SetTheory.PGame} {z : SetTheory.PGame} (h : y.LF z) (x : SetTheory.PGame) :
                                                                                                (y + x).LF (z + x)
                                                                                                theorem SetTheory.PGame.add_lf_add_left {y : SetTheory.PGame} {z : SetTheory.PGame} (h : y.LF z) (x : SetTheory.PGame) :
                                                                                                (x + y).LF (x + z)
                                                                                                theorem SetTheory.PGame.add_lf_add_of_lf_of_le {w : SetTheory.PGame} {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (hwx : w.LF x) (hyz : y z) :
                                                                                                (w + y).LF (x + z)
                                                                                                theorem SetTheory.PGame.add_lf_add_of_le_of_lf {w : SetTheory.PGame} {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (hwx : w x) (hyz : y.LF z) :
                                                                                                (w + y).LF (x + z)
                                                                                                theorem SetTheory.PGame.add_congr {w : SetTheory.PGame} {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : w x) (h₂ : y z) :
                                                                                                w + y x + z
                                                                                                theorem SetTheory.PGame.sub_congr {w : SetTheory.PGame} {x : SetTheory.PGame} {y : SetTheory.PGame} {z : SetTheory.PGame} (h₁ : w x) (h₂ : y z) :
                                                                                                w - y x - z

                                                                                                Inserting an option #

                                                                                                The pregame constructed by inserting x' as a new left option into x.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  theorem SetTheory.PGame.le_insertLeft (x : SetTheory.PGame) (x' : SetTheory.PGame) :
                                                                                                  x x.insertLeft x'

                                                                                                  A new left option cannot hurt Left.

                                                                                                  theorem SetTheory.PGame.insertLeft_equiv_of_lf {x : SetTheory.PGame} {x' : SetTheory.PGame} (h : x'.LF x) :
                                                                                                  x.insertLeft x' x

                                                                                                  Adding a gift horse left option does not change the value of x. A gift horse left option is a game x' with x' ⧏ x. It is called "gift horse" because it seems like Left has gotten the "gift" of a new option, but actually the value of the game did not change.

                                                                                                  The pregame constructed by inserting x' as a new right option into x.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    theorem SetTheory.PGame.neg_insertRight_neg (x : SetTheory.PGame) (x' : SetTheory.PGame) :
                                                                                                    (-x).insertRight (-x') = -x.insertLeft x'
                                                                                                    theorem SetTheory.PGame.neg_insertLeft_neg (x : SetTheory.PGame) (x' : SetTheory.PGame) :
                                                                                                    (-x).insertLeft (-x') = -x.insertRight x'
                                                                                                    theorem SetTheory.PGame.insertRight_le (x : SetTheory.PGame) (x' : SetTheory.PGame) :
                                                                                                    x.insertRight x' x

                                                                                                    A new right option cannot hurt Right.

                                                                                                    theorem SetTheory.PGame.insertRight_equiv_of_lf {x : SetTheory.PGame} {x' : SetTheory.PGame} (h : x.LF x') :
                                                                                                    x.insertRight x' x

                                                                                                    Adding a gift horse right option does not change the value of x. A gift horse right option is a game x' with x ⧏ x'. It is called "gift horse" because it seems like Right has gotten the "gift" of a new option, but actually the value of the game did not change.

                                                                                                    theorem SetTheory.PGame.insertRight_insertLeft {x : SetTheory.PGame} {x' : SetTheory.PGame} {x'' : SetTheory.PGame} :
                                                                                                    (x.insertLeft x').insertRight x'' = (x.insertRight x'').insertLeft x'

                                                                                                    Inserting on the left and right commutes.

                                                                                                    Special pre-games #

                                                                                                    The pre-game star, which is fuzzy with zero.

                                                                                                    Equations
                                                                                                    Instances For