[GOAL]
x✝ x : PGame
IHl : ∀ (i : LeftMoves x), Acc IsOption (moveLeft x i)
IHr : ∀ (j : RightMoves x), Acc IsOption (moveRight x j)
y : PGame
h : IsOption y x
⊢ Acc IsOption y
[PROOFSTEP]
induction' h with _ i _ j
[GOAL]
case moveLeft
x✝¹ x : PGame
IHl✝ : ∀ (i : LeftMoves x), Acc IsOption (moveLeft x i)
IHr✝ : ∀ (j : RightMoves x), Acc IsOption (moveRight x j)
y x✝ : PGame
i : LeftMoves x✝
IHl : ∀ (i : LeftMoves x✝), Acc IsOption (moveLeft x✝ i)
IHr : ∀ (j : RightMoves x✝), Acc IsOption (moveRight x✝ j)
⊢ Acc IsOption (moveLeft x✝ i)
[PROOFSTEP]
exact IHl i
[GOAL]
case moveRight
x✝¹ x : PGame
IHl✝ : ∀ (i : LeftMoves x), Acc IsOption (moveLeft x i)
IHr✝ : ∀ (j : RightMoves x), Acc IsOption (moveRight x j)
y x✝ : PGame
j : RightMoves x✝
IHl : ∀ (i : LeftMoves x✝), Acc IsOption (moveLeft x✝ i)
IHr : ∀ (j : RightMoves x✝), Acc IsOption (moveRight x✝ j)
⊢ Acc IsOption (moveRight x✝ j)
[PROOFSTEP]
exact IHr j
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
j : RightMoves (mk xl xr xL xR)
⊢ Subsequent (xR j) (mk xl xr xL xR)
[PROOFSTEP]
pgame_wf_tac
[GOAL]
xl : Type u_1
i : xl
xr : Type u_1
xR : xr → PGame
xL : xl → PGame
j : RightMoves (xL i)
⊢ Subsequent (PGame.moveRight (xL i) j) (mk xl xr xL xR)
[PROOFSTEP]
pgame_wf_tac
[GOAL]
xr : Type u_1
i : xr
xl : Type u_1
xL : xl → PGame
xR : xr → PGame
j : RightMoves (xR i)
⊢ Subsequent (PGame.moveRight (xR i) j) (mk xl xr xL xR)
[PROOFSTEP]
pgame_wf_tac
[GOAL]
xl : Type u_1
i : xl
xr : Type u_1
xR : xr → PGame
xL : xl → PGame
j : LeftMoves (xL i)
⊢ Subsequent (PGame.moveLeft (xL i) j) (mk xl xr xL xR)
[PROOFSTEP]
pgame_wf_tac
[GOAL]
xr : Type u_1
i : xr
xl : Type u_1
xL : xl → PGame
xR : xr → PGame
j : LeftMoves (xR i)
⊢ Subsequent (PGame.moveLeft (xR i) j) (mk xl xr xL xR)
[PROOFSTEP]
pgame_wf_tac
  -- Porting note: linter claims these lemmas don't simplify?
[GOAL]
x y : PGame
⊢ x ≤ y ↔ (∀ (i : LeftMoves x), moveLeft x i ⧏ y) ∧ ∀ (j : RightMoves y), x ⧏ moveRight y j
[PROOFSTEP]
unfold LE.le le
[GOAL]
x y : PGame
⊢ {
          le :=
            Sym2.GameAdd.fix wf_isOption fun x y le =>
              (∀ (i : LeftMoves x),
                  ¬le y (moveLeft x i)
                      (_ :
                        Sym2.GameAdd IsOption (Quotient.mk (Sym2.Rel.setoid PGame) (y, moveLeft x i))
                          (Quotient.mk (Sym2.Rel.setoid PGame) (x, y)))) ∧
                ∀ (j : RightMoves y),
                  ¬le (moveRight y j) x
                      (_ :
                        Sym2.GameAdd IsOption (Quotient.mk (Sym2.Rel.setoid PGame) (moveRight y j, x))
                          (Quotient.mk (Sym2.Rel.setoid PGame) (x, y))) }.1
      x y ↔
    (∀ (i : LeftMoves x), moveLeft x i ⧏ y) ∧ ∀ (j : RightMoves y), x ⧏ moveRight y j
[PROOFSTEP]
simp only
[GOAL]
x y : PGame
⊢ Sym2.GameAdd.fix wf_isOption
      (fun x y le =>
        (∀ (i : LeftMoves x),
            ¬le y (moveLeft x i)
                (_ :
                  Sym2.GameAdd IsOption (Quotient.mk (Sym2.Rel.setoid PGame) (y, moveLeft x i))
                    (Quotient.mk (Sym2.Rel.setoid PGame) (x, y)))) ∧
          ∀ (j : RightMoves y),
            ¬le (moveRight y j) x
                (_ :
                  Sym2.GameAdd IsOption (Quotient.mk (Sym2.Rel.setoid PGame) (moveRight y j, x))
                    (Quotient.mk (Sym2.Rel.setoid PGame) (x, y))))
      x y ↔
    (∀ (i : LeftMoves x), moveLeft x i ⧏ y) ∧ ∀ (j : RightMoves y), x ⧏ moveRight y j
[PROOFSTEP]
rw [Sym2.GameAdd.fix_eq]
[GOAL]
x y : PGame
⊢ ((∀ (i : LeftMoves x),
        ¬(fun a' b' x =>
              Sym2.GameAdd.fix wf_isOption
                (fun x y le =>
                  (∀ (i : LeftMoves x),
                      ¬le y (moveLeft x i)
                          (_ :
                            Sym2.GameAdd IsOption (Quotient.mk (Sym2.Rel.setoid PGame) (y, moveLeft x i))
                              (Quotient.mk (Sym2.Rel.setoid PGame) (x, y)))) ∧
                    ∀ (j : RightMoves y),
                      ¬le (moveRight y j) x
                          (_ :
                            Sym2.GameAdd IsOption (Quotient.mk (Sym2.Rel.setoid PGame) (moveRight y j, x))
                              (Quotient.mk (Sym2.Rel.setoid PGame) (x, y))))
                a' b')
            y (moveLeft x i)
            (_ :
              Sym2.GameAdd IsOption (Quotient.mk (Sym2.Rel.setoid PGame) (y, moveLeft x i))
                (Quotient.mk (Sym2.Rel.setoid PGame) (x, y)))) ∧
      ∀ (j : RightMoves y),
        ¬(fun a' b' x =>
              Sym2.GameAdd.fix wf_isOption
                (fun x y le =>
                  (∀ (i : LeftMoves x),
                      ¬le y (moveLeft x i)
                          (_ :
                            Sym2.GameAdd IsOption (Quotient.mk (Sym2.Rel.setoid PGame) (y, moveLeft x i))
                              (Quotient.mk (Sym2.Rel.setoid PGame) (x, y)))) ∧
                    ∀ (j : RightMoves y),
                      ¬le (moveRight y j) x
                          (_ :
                            Sym2.GameAdd IsOption (Quotient.mk (Sym2.Rel.setoid PGame) (moveRight y j, x))
                              (Quotient.mk (Sym2.Rel.setoid PGame) (x, y))))
                a' b')
            (moveRight y j) x
            (_ :
              Sym2.GameAdd IsOption (Quotient.mk (Sym2.Rel.setoid PGame) (moveRight y j, x))
                (Quotient.mk (Sym2.Rel.setoid PGame) (x, y)))) ↔
    (∀ (i : LeftMoves x), moveLeft x i ⧏ y) ∧ ∀ (j : RightMoves y), x ⧏ moveRight y j
[PROOFSTEP]
rfl
[GOAL]
x y : PGame
⊢ x ⧏ y ↔ (∃ i, x ≤ moveLeft y i) ∨ ∃ j, moveRight x j ≤ y
[PROOFSTEP]
rw [Lf, le_iff_forall_lf, not_and_or]
[GOAL]
x y : PGame
⊢ ((¬∀ (i : LeftMoves y), moveLeft y i ⧏ x) ∨ ¬∀ (j : RightMoves x), y ⧏ moveRight x j) ↔
    (∃ i, x ≤ moveLeft y i) ∨ ∃ j, moveRight x j ≤ y
[PROOFSTEP]
simp
[GOAL]
x y : PGame
⊢ x ≤ y ∨ y ⧏ x
[PROOFSTEP]
rw [← PGame.not_le]
[GOAL]
x y : PGame
⊢ x ≤ y ∨ ¬x ≤ y
[PROOFSTEP]
apply em
[GOAL]
src✝ : LE PGame := le
x : PGame
⊢ x ≤ x
[PROOFSTEP]
induction' x with _ _ _ _ IHl IHr
[GOAL]
case mk
src✝ : LE PGame := le
α✝ β✝ : Type ?u.34536
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
IHl : ∀ (a : α✝), a✝¹ a ≤ a✝¹ a
IHr : ∀ (a : β✝), a✝ a ≤ a✝ a
⊢ mk α✝ β✝ a✝¹ a✝ ≤ mk α✝ β✝ a✝¹ a✝
[PROOFSTEP]
exact le_of_forall_lf (fun i => lf_of_le_moveLeft (IHl i)) fun i => lf_of_moveRight_le (IHr i)
[GOAL]
src✝ : LE PGame := le
⊢ ∀ (a b c : PGame), a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
suffices : ∀ {x y z : PGame}, (x ≤ y → y ≤ z → x ≤ z) ∧ (y ≤ z → z ≤ x → y ≤ x) ∧ (z ≤ x → x ≤ y → z ≤ y)
[GOAL]
src✝ : LE PGame := le
this : ∀ {x y z : PGame}, (x ≤ y → y ≤ z → x ≤ z) ∧ (y ≤ z → z ≤ x → y ≤ x) ∧ (z ≤ x → x ≤ y → z ≤ y)
⊢ ∀ (a b c : PGame), a ≤ b → b ≤ c → a ≤ c
case this
src✝ : LE PGame := le
⊢ ∀ {x y z : PGame}, (x ≤ y → y ≤ z → x ≤ z) ∧ (y ≤ z → z ≤ x → y ≤ x) ∧ (z ≤ x → x ≤ y → z ≤ y)
[PROOFSTEP]
exact fun x y z => this.1
[GOAL]
case this
src✝ : LE PGame := le
⊢ ∀ {x y z : PGame}, (x ≤ y → y ≤ z → x ≤ z) ∧ (y ≤ z → z ≤ x → y ≤ x) ∧ (z ≤ x → x ≤ y → z ≤ y)
[PROOFSTEP]
intro x y z
[GOAL]
case this
src✝ : LE PGame := le
x y z : PGame
⊢ (x ≤ y → y ≤ z → x ≤ z) ∧ (y ≤ z → z ≤ x → y ≤ x) ∧ (z ≤ x → x ≤ y → z ≤ y)
[PROOFSTEP]
induction' x with xl xr xL xR IHxl IHxr generalizing y z
[GOAL]
case this.mk
src✝ : LE PGame := le
y✝ z✝ : PGame
xl xr : Type ?u.34927
xL : xl → PGame
xR : xr → PGame
IHxl :
  ∀ (a : xl) {y z : PGame},
    (xL a ≤ y → y ≤ z → xL a ≤ z) ∧ (y ≤ z → z ≤ xL a → y ≤ xL a) ∧ (z ≤ xL a → xL a ≤ y → z ≤ y)
IHxr :
  ∀ (a : xr) {y z : PGame},
    (xR a ≤ y → y ≤ z → xR a ≤ z) ∧ (y ≤ z → z ≤ xR a → y ≤ xR a) ∧ (z ≤ xR a → xR a ≤ y → z ≤ y)
y z : PGame
⊢ (mk xl xr xL xR ≤ y → y ≤ z → mk xl xr xL xR ≤ z) ∧
    (y ≤ z → z ≤ mk xl xr xL xR → y ≤ mk xl xr xL xR) ∧ (z ≤ mk xl xr xL xR → mk xl xr xL xR ≤ y → z ≤ y)
[PROOFSTEP]
induction' y with yl yr yL yR IHyl IHyr generalizing z
[GOAL]
case this.mk.mk
src✝ : LE PGame := le
y z✝¹ : PGame
xl xr : Type ?u.34969
xL : xl → PGame
xR : xr → PGame
IHxl :
  ∀ (a : xl) {y z : PGame},
    (xL a ≤ y → y ≤ z → xL a ≤ z) ∧ (y ≤ z → z ≤ xL a → y ≤ xL a) ∧ (z ≤ xL a → xL a ≤ y → z ≤ y)
IHxr :
  ∀ (a : xr) {y z : PGame},
    (xR a ≤ y → y ≤ z → xR a ≤ z) ∧ (y ≤ z → z ≤ xR a → y ≤ xR a) ∧ (z ≤ xR a → xR a ≤ y → z ≤ y)
z✝ : PGame
yl yr : Type ?u.34969
yL : yl → PGame
yR : yr → PGame
IHyl :
  ∀ (a : yl) {z : PGame},
    (mk xl xr xL xR ≤ yL a → yL a ≤ z → mk xl xr xL xR ≤ z) ∧
      (yL a ≤ z → z ≤ mk xl xr xL xR → yL a ≤ mk xl xr xL xR) ∧ (z ≤ mk xl xr xL xR → mk xl xr xL xR ≤ yL a → z ≤ yL a)
IHyr :
  ∀ (a : yr) {z : PGame},
    (mk xl xr xL xR ≤ yR a → yR a ≤ z → mk xl xr xL xR ≤ z) ∧
      (yR a ≤ z → z ≤ mk xl xr xL xR → yR a ≤ mk xl xr xL xR) ∧ (z ≤ mk xl xr xL xR → mk xl xr xL xR ≤ yR a → z ≤ yR a)
z : PGame
⊢ (mk xl xr xL xR ≤ mk yl yr yL yR → mk yl yr yL yR ≤ z → mk xl xr xL xR ≤ z) ∧
    (mk yl yr yL yR ≤ z → z ≤ mk xl xr xL xR → mk yl yr yL yR ≤ mk xl xr xL xR) ∧
      (z ≤ mk xl xr xL xR → mk xl xr xL xR ≤ mk yl yr yL yR → z ≤ mk yl yr yL yR)
[PROOFSTEP]
induction' z with zl zr zL zR IHzl IHzr
[GOAL]
case this.mk.mk.mk
src✝ : LE PGame := le
y z✝ : PGame
xl xr : Type ?u.35006
xL : xl → PGame
xR : xr → PGame
IHxl :
  ∀ (a : xl) {y z : PGame},
    (xL a ≤ y → y ≤ z → xL a ≤ z) ∧ (y ≤ z → z ≤ xL a → y ≤ xL a) ∧ (z ≤ xL a → xL a ≤ y → z ≤ y)
IHxr :
  ∀ (a : xr) {y z : PGame},
    (xR a ≤ y → y ≤ z → xR a ≤ z) ∧ (y ≤ z → z ≤ xR a → y ≤ xR a) ∧ (z ≤ xR a → xR a ≤ y → z ≤ y)
z : PGame
yl yr : Type ?u.35006
yL : yl → PGame
yR : yr → PGame
IHyl :
  ∀ (a : yl) {z : PGame},
    (mk xl xr xL xR ≤ yL a → yL a ≤ z → mk xl xr xL xR ≤ z) ∧
      (yL a ≤ z → z ≤ mk xl xr xL xR → yL a ≤ mk xl xr xL xR) ∧ (z ≤ mk xl xr xL xR → mk xl xr xL xR ≤ yL a → z ≤ yL a)
IHyr :
  ∀ (a : yr) {z : PGame},
    (mk xl xr xL xR ≤ yR a → yR a ≤ z → mk xl xr xL xR ≤ z) ∧
      (yR a ≤ z → z ≤ mk xl xr xL xR → yR a ≤ mk xl xr xL xR) ∧ (z ≤ mk xl xr xL xR → mk xl xr xL xR ≤ yR a → z ≤ yR a)
zl zr : Type ?u.35006
zL : zl → PGame
zR : zr → PGame
IHzl :
  ∀ (a : zl),
    (mk xl xr xL xR ≤ mk yl yr yL yR → mk yl yr yL yR ≤ zL a → mk xl xr xL xR ≤ zL a) ∧
      (mk yl yr yL yR ≤ zL a → zL a ≤ mk xl xr xL xR → mk yl yr yL yR ≤ mk xl xr xL xR) ∧
        (zL a ≤ mk xl xr xL xR → mk xl xr xL xR ≤ mk yl yr yL yR → zL a ≤ mk yl yr yL yR)
IHzr :
  ∀ (a : zr),
    (mk xl xr xL xR ≤ mk yl yr yL yR → mk yl yr yL yR ≤ zR a → mk xl xr xL xR ≤ zR a) ∧
      (mk yl yr yL yR ≤ zR a → zR a ≤ mk xl xr xL xR → mk yl yr yL yR ≤ mk xl xr xL xR) ∧
        (zR a ≤ mk xl xr xL xR → mk xl xr xL xR ≤ mk yl yr yL yR → zR a ≤ mk yl yr yL yR)
⊢ (mk xl xr xL xR ≤ mk yl yr yL yR → mk yl yr yL yR ≤ mk zl zr zL zR → mk xl xr xL xR ≤ mk zl zr zL zR) ∧
    (mk yl yr yL yR ≤ mk zl zr zL zR → mk zl zr zL zR ≤ mk xl xr xL xR → mk yl yr yL yR ≤ mk xl xr xL xR) ∧
      (mk zl zr zL zR ≤ mk xl xr xL xR → mk xl xr xL xR ≤ mk yl yr yL yR → mk zl zr zL zR ≤ mk yl yr yL yR)
[PROOFSTEP]
exact
  ⟨le_trans_aux (fun {i} => (IHxl i).2.1) fun {j} => (IHzr j).2.2,
    le_trans_aux (fun {i} => (IHyl i).2.2) fun {j} => (IHxr j).1,
    le_trans_aux (fun {i} => (IHzl i).1) fun {j} => (IHyr j).2.1⟩
[GOAL]
x y z : PGame
h₁ : x ≤ y
h₂ : y ⧏ z
⊢ x ⧏ z
[PROOFSTEP]
rw [← PGame.not_le] at h₂ ⊢
[GOAL]
x y z : PGame
h₁ : x ≤ y
h₂ : ¬z ≤ y
⊢ ¬z ≤ x
[PROOFSTEP]
exact fun h₃ => h₂ (h₃.trans h₁)
[GOAL]
x y z : PGame
h₁ : x ⧏ y
h₂ : y ≤ z
⊢ x ⧏ z
[PROOFSTEP]
rw [← PGame.not_le] at h₁ ⊢
[GOAL]
x y z : PGame
h₁ : ¬y ≤ x
h₂ : y ≤ z
⊢ ¬z ≤ x
[PROOFSTEP]
exact fun h₃ => h₁ (h₂.trans h₃)
[GOAL]
x y : PGame
⊢ x ≤ y ↔
    (∀ (i : LeftMoves x), (∃ i', moveLeft x i ≤ moveLeft y i') ∨ ∃ j, moveRight (moveLeft x i) j ≤ y) ∧
      ∀ (j : RightMoves y), (∃ i, x ≤ moveLeft (moveRight y j) i) ∨ ∃ j', moveRight x j' ≤ moveRight y j
[PROOFSTEP]
rw [le_iff_forall_lf]
[GOAL]
x y : PGame
⊢ ((∀ (i : LeftMoves x), moveLeft x i ⧏ y) ∧ ∀ (j : RightMoves y), x ⧏ moveRight y j) ↔
    (∀ (i : LeftMoves x), (∃ i', moveLeft x i ≤ moveLeft y i') ∨ ∃ j, moveRight (moveLeft x i) j ≤ y) ∧
      ∀ (j : RightMoves y), (∃ i, x ≤ moveLeft (moveRight y j) i) ∨ ∃ j', moveRight x j' ≤ moveRight y j
[PROOFSTEP]
conv =>
  lhs
  simp only [lf_iff_exists_le]
[GOAL]
x y : PGame
| ((∀ (i : LeftMoves x), moveLeft x i ⧏ y) ∧ ∀ (j : RightMoves y), x ⧏ moveRight y j) ↔
    (∀ (i : LeftMoves x), (∃ i', moveLeft x i ≤ moveLeft y i') ∨ ∃ j, moveRight (moveLeft x i) j ≤ y) ∧
      ∀ (j : RightMoves y), (∃ i, x ≤ moveLeft (moveRight y j) i) ∨ ∃ j', moveRight x j' ≤ moveRight y j
[PROOFSTEP]
  lhs
  simp only [lf_iff_exists_le]
[GOAL]
x y : PGame
| ((∀ (i : LeftMoves x), moveLeft x i ⧏ y) ∧ ∀ (j : RightMoves y), x ⧏ moveRight y j) ↔
    (∀ (i : LeftMoves x), (∃ i', moveLeft x i ≤ moveLeft y i') ∨ ∃ j, moveRight (moveLeft x i) j ≤ y) ∧
      ∀ (j : RightMoves y), (∃ i, x ≤ moveLeft (moveRight y j) i) ∨ ∃ j', moveRight x j' ≤ moveRight y j
[PROOFSTEP]
  lhs
  simp only [lf_iff_exists_le]
[GOAL]
x y : PGame
| ((∀ (i : LeftMoves x), moveLeft x i ⧏ y) ∧ ∀ (j : RightMoves y), x ⧏ moveRight y j) ↔
    (∀ (i : LeftMoves x), (∃ i', moveLeft x i ≤ moveLeft y i') ∨ ∃ j, moveRight (moveLeft x i) j ≤ y) ∧
      ∀ (j : RightMoves y), (∃ i, x ≤ moveLeft (moveRight y j) i) ∨ ∃ j', moveRight x j' ≤ moveRight y j
[PROOFSTEP]
lhs
[GOAL]
x y : PGame
| (∀ (i : LeftMoves x), moveLeft x i ⧏ y) ∧ ∀ (j : RightMoves y), x ⧏ moveRight y j
[PROOFSTEP]
simp only [lf_iff_exists_le]
[GOAL]
x y : PGame
⊢ x ⧏ y ↔
    (∃ i,
        (∀ (i' : LeftMoves x), moveLeft x i' ⧏ moveLeft y i) ∧
          ∀ (j : RightMoves (moveLeft y i)), x ⧏ moveRight (moveLeft y i) j) ∨
      ∃ j,
        (∀ (i : LeftMoves (moveRight x j)), moveLeft (moveRight x j) i ⧏ y) ∧
          ∀ (j' : RightMoves y), moveRight x j ⧏ moveRight y j'
[PROOFSTEP]
rw [lf_iff_exists_le]
[GOAL]
x y : PGame
⊢ ((∃ i, x ≤ moveLeft y i) ∨ ∃ j, moveRight x j ≤ y) ↔
    (∃ i,
        (∀ (i' : LeftMoves x), moveLeft x i' ⧏ moveLeft y i) ∧
          ∀ (j : RightMoves (moveLeft y i)), x ⧏ moveRight (moveLeft y i) j) ∨
      ∃ j,
        (∀ (i : LeftMoves (moveRight x j)), moveLeft (moveRight x j) i ⧏ y) ∧
          ∀ (j' : RightMoves y), moveRight x j ⧏ moveRight y j'
[PROOFSTEP]
conv =>
  lhs
  simp only [le_iff_forall_lf]
[GOAL]
x y : PGame
| ((∃ i, x ≤ moveLeft y i) ∨ ∃ j, moveRight x j ≤ y) ↔
    (∃ i,
        (∀ (i' : LeftMoves x), moveLeft x i' ⧏ moveLeft y i) ∧
          ∀ (j : RightMoves (moveLeft y i)), x ⧏ moveRight (moveLeft y i) j) ∨
      ∃ j,
        (∀ (i : LeftMoves (moveRight x j)), moveLeft (moveRight x j) i ⧏ y) ∧
          ∀ (j' : RightMoves y), moveRight x j ⧏ moveRight y j'
[PROOFSTEP]
  lhs
  simp only [le_iff_forall_lf]
[GOAL]
x y : PGame
| ((∃ i, x ≤ moveLeft y i) ∨ ∃ j, moveRight x j ≤ y) ↔
    (∃ i,
        (∀ (i' : LeftMoves x), moveLeft x i' ⧏ moveLeft y i) ∧
          ∀ (j : RightMoves (moveLeft y i)), x ⧏ moveRight (moveLeft y i) j) ∨
      ∃ j,
        (∀ (i : LeftMoves (moveRight x j)), moveLeft (moveRight x j) i ⧏ y) ∧
          ∀ (j' : RightMoves y), moveRight x j ⧏ moveRight y j'
[PROOFSTEP]
  lhs
  simp only [le_iff_forall_lf]
[GOAL]
x y : PGame
| ((∃ i, x ≤ moveLeft y i) ∨ ∃ j, moveRight x j ≤ y) ↔
    (∃ i,
        (∀ (i' : LeftMoves x), moveLeft x i' ⧏ moveLeft y i) ∧
          ∀ (j : RightMoves (moveLeft y i)), x ⧏ moveRight (moveLeft y i) j) ∨
      ∃ j,
        (∀ (i : LeftMoves (moveRight x j)), moveLeft (moveRight x j) i ⧏ y) ∧
          ∀ (j' : RightMoves y), moveRight x j ⧏ moveRight y j'
[PROOFSTEP]
lhs
[GOAL]
x y : PGame
| (∃ i, x ≤ moveLeft y i) ∨ ∃ j, moveRight x j ≤ y
[PROOFSTEP]
simp only [le_iff_forall_lf]
[GOAL]
x : PGame
⊢ 0 ≤ x ↔ ∀ (j : RightMoves x), 0 ⧏ moveRight x j
[PROOFSTEP]
rw [le_iff_forall_lf]
[GOAL]
x : PGame
⊢ ((∀ (i : LeftMoves 0), moveLeft 0 i ⧏ x) ∧ ∀ (j : RightMoves x), 0 ⧏ moveRight x j) ↔
    ∀ (j : RightMoves x), 0 ⧏ moveRight x j
[PROOFSTEP]
simp
[GOAL]
x : PGame
⊢ x ≤ 0 ↔ ∀ (i : LeftMoves x), moveLeft x i ⧏ 0
[PROOFSTEP]
rw [le_iff_forall_lf]
[GOAL]
x : PGame
⊢ ((∀ (i : LeftMoves x), moveLeft x i ⧏ 0) ∧ ∀ (j : RightMoves 0), x ⧏ moveRight 0 j) ↔
    ∀ (i : LeftMoves x), moveLeft x i ⧏ 0
[PROOFSTEP]
simp
[GOAL]
x : PGame
⊢ 0 ⧏ x ↔ ∃ i, 0 ≤ moveLeft x i
[PROOFSTEP]
rw [lf_iff_exists_le]
[GOAL]
x : PGame
⊢ ((∃ i, 0 ≤ moveLeft x i) ∨ ∃ j, moveRight 0 j ≤ x) ↔ ∃ i, 0 ≤ moveLeft x i
[PROOFSTEP]
simp
[GOAL]
x : PGame
⊢ x ⧏ 0 ↔ ∃ j, moveRight x j ≤ 0
[PROOFSTEP]
rw [lf_iff_exists_le]
[GOAL]
x : PGame
⊢ ((∃ i, x ≤ moveLeft 0 i) ∨ ∃ j, moveRight x j ≤ 0) ↔ ∃ j, moveRight x j ≤ 0
[PROOFSTEP]
simp
[GOAL]
x : PGame
⊢ 0 ≤ x ↔ ∀ (j : RightMoves x), ∃ i, 0 ≤ moveLeft (moveRight x j) i
[PROOFSTEP]
rw [le_def]
[GOAL]
x : PGame
⊢ ((∀ (i : LeftMoves 0), (∃ i', moveLeft 0 i ≤ moveLeft x i') ∨ ∃ j, moveRight (moveLeft 0 i) j ≤ x) ∧
      ∀ (j : RightMoves x), (∃ i, 0 ≤ moveLeft (moveRight x j) i) ∨ ∃ j', moveRight 0 j' ≤ moveRight x j) ↔
    ∀ (j : RightMoves x), ∃ i, 0 ≤ moveLeft (moveRight x j) i
[PROOFSTEP]
simp
[GOAL]
x : PGame
⊢ x ≤ 0 ↔ ∀ (i : LeftMoves x), ∃ j, moveRight (moveLeft x i) j ≤ 0
[PROOFSTEP]
rw [le_def]
[GOAL]
x : PGame
⊢ ((∀ (i : LeftMoves x), (∃ i', moveLeft x i ≤ moveLeft 0 i') ∨ ∃ j, moveRight (moveLeft x i) j ≤ 0) ∧
      ∀ (j : RightMoves 0), (∃ i, x ≤ moveLeft (moveRight 0 j) i) ∨ ∃ j', moveRight x j' ≤ moveRight 0 j) ↔
    ∀ (i : LeftMoves x), ∃ j, moveRight (moveLeft x i) j ≤ 0
[PROOFSTEP]
simp
[GOAL]
x : PGame
⊢ 0 ⧏ x ↔ ∃ i, ∀ (j : RightMoves (moveLeft x i)), 0 ⧏ moveRight (moveLeft x i) j
[PROOFSTEP]
rw [lf_def]
[GOAL]
x : PGame
⊢ ((∃ i,
        (∀ (i' : LeftMoves 0), moveLeft 0 i' ⧏ moveLeft x i) ∧
          ∀ (j : RightMoves (moveLeft x i)), 0 ⧏ moveRight (moveLeft x i) j) ∨
      ∃ j,
        (∀ (i : LeftMoves (moveRight 0 j)), moveLeft (moveRight 0 j) i ⧏ x) ∧
          ∀ (j' : RightMoves x), moveRight 0 j ⧏ moveRight x j') ↔
    ∃ i, ∀ (j : RightMoves (moveLeft x i)), 0 ⧏ moveRight (moveLeft x i) j
[PROOFSTEP]
simp
[GOAL]
x : PGame
⊢ x ⧏ 0 ↔ ∃ j, ∀ (i : LeftMoves (moveRight x j)), moveLeft (moveRight x j) i ⧏ 0
[PROOFSTEP]
rw [lf_def]
[GOAL]
x : PGame
⊢ ((∃ i,
        (∀ (i' : LeftMoves x), moveLeft x i' ⧏ moveLeft 0 i) ∧
          ∀ (j : RightMoves (moveLeft 0 i)), x ⧏ moveRight (moveLeft 0 i) j) ∨
      ∃ j,
        (∀ (i : LeftMoves (moveRight x j)), moveLeft (moveRight x j) i ⧏ 0) ∧
          ∀ (j' : RightMoves 0), moveRight x j ⧏ moveRight 0 j') ↔
    ∃ j, ∀ (i : LeftMoves (moveRight x j)), moveLeft (moveRight x j) i ⧏ 0
[PROOFSTEP]
simp
[GOAL]
x y : PGame
h : x = y
⊢ x ≈ y
[PROOFSTEP]
subst h
[GOAL]
x : PGame
⊢ x ≈ x
[PROOFSTEP]
rfl
[GOAL]
x y : PGame
⊢ x ⧏ y ∨ x ≈ y ∨ y ⧏ x
[PROOFSTEP]
by_cases h : x ⧏ y
[GOAL]
case pos
x y : PGame
h : x ⧏ y
⊢ x ⧏ y ∨ x ≈ y ∨ y ⧏ x
[PROOFSTEP]
exact Or.inl h
[GOAL]
case neg
x y : PGame
h : ¬x ⧏ y
⊢ x ⧏ y ∨ x ≈ y ∨ y ⧏ x
[PROOFSTEP]
right
[GOAL]
case neg.h
x y : PGame
h : ¬x ⧏ y
⊢ x ≈ y ∨ y ⧏ x
[PROOFSTEP]
cases' lt_or_equiv_of_le (PGame.not_lf.1 h) with h' h'
[GOAL]
case neg.h.inl
x y : PGame
h : ¬x ⧏ y
h' : y < x
⊢ x ≈ y ∨ y ⧏ x
[PROOFSTEP]
exact Or.inr h'.lf
[GOAL]
case neg.h.inr
x y : PGame
h : ¬x ⧏ y
h' : y ≈ x
⊢ x ≈ y ∨ y ⧏ x
[PROOFSTEP]
exact Or.inl (Equiv.symm h')
[GOAL]
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hl : ∀ (i : LeftMoves x), moveLeft x i ≈ moveLeft y (↑L i)
hr : ∀ (j : RightMoves x), moveRight x j ≈ moveRight y (↑R j)
⊢ x ≈ y
[PROOFSTEP]
constructor
[GOAL]
case left
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hl : ∀ (i : LeftMoves x), moveLeft x i ≈ moveLeft y (↑L i)
hr : ∀ (j : RightMoves x), moveRight x j ≈ moveRight y (↑R j)
⊢ x ≤ y
[PROOFSTEP]
rw [le_def]
[GOAL]
case right
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hl : ∀ (i : LeftMoves x), moveLeft x i ≈ moveLeft y (↑L i)
hr : ∀ (j : RightMoves x), moveRight x j ≈ moveRight y (↑R j)
⊢ y ≤ x
[PROOFSTEP]
rw [le_def]
[GOAL]
case left
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hl : ∀ (i : LeftMoves x), moveLeft x i ≈ moveLeft y (↑L i)
hr : ∀ (j : RightMoves x), moveRight x j ≈ moveRight y (↑R j)
⊢ (∀ (i : LeftMoves x), (∃ i', moveLeft x i ≤ moveLeft y i') ∨ ∃ j, moveRight (moveLeft x i) j ≤ y) ∧
    ∀ (j : RightMoves y), (∃ i, x ≤ moveLeft (moveRight y j) i) ∨ ∃ j', moveRight x j' ≤ moveRight y j
[PROOFSTEP]
exact ⟨fun i => Or.inl ⟨_, (hl i).1⟩, fun j => Or.inr ⟨_, by simpa using (hr (R.symm j)).1⟩⟩
[GOAL]
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hl : ∀ (i : LeftMoves x), moveLeft x i ≈ moveLeft y (↑L i)
hr : ∀ (j : RightMoves x), moveRight x j ≈ moveRight y (↑R j)
j : RightMoves y
⊢ moveRight x (?m.65380 j) ≤ moveRight y j
[PROOFSTEP]
simpa using (hr (R.symm j)).1
[GOAL]
case right
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hl : ∀ (i : LeftMoves x), moveLeft x i ≈ moveLeft y (↑L i)
hr : ∀ (j : RightMoves x), moveRight x j ≈ moveRight y (↑R j)
⊢ (∀ (i : LeftMoves y), (∃ i', moveLeft y i ≤ moveLeft x i') ∨ ∃ j, moveRight (moveLeft y i) j ≤ x) ∧
    ∀ (j : RightMoves x), (∃ i, y ≤ moveLeft (moveRight x j) i) ∨ ∃ j', moveRight y j' ≤ moveRight x j
[PROOFSTEP]
exact ⟨fun i => Or.inl ⟨_, by simpa using (hl (L.symm i)).2⟩, fun j => Or.inr ⟨_, (hr j).2⟩⟩
[GOAL]
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hl : ∀ (i : LeftMoves x), moveLeft x i ≈ moveLeft y (↑L i)
hr : ∀ (j : RightMoves x), moveRight x j ≈ moveRight y (↑R j)
i : LeftMoves y
⊢ moveLeft y i ≤ moveLeft x (?m.66064 i)
[PROOFSTEP]
simpa using (hl (L.symm i)).2
[GOAL]
x y : PGame
⊢ x ⧏ y ↔ x < y ∨ x ‖ y
[PROOFSTEP]
simp only [lt_iff_le_and_lf, Fuzzy, ← PGame.not_le]
[GOAL]
x y : PGame
⊢ ¬y ≤ x ↔ x ≤ y ∧ ¬y ≤ x ∨ ¬y ≤ x ∧ ¬x ≤ y
[PROOFSTEP]
tauto
[GOAL]
x₁ y₁ x₂ y₂ : PGame
hx : x₁ ≈ x₂
hy : y₁ ≈ y₂
⊢ x₁ ⧏ y₁ ∧ y₁ ⧏ x₁ ↔ x₂ ⧏ y₂ ∧ y₂ ⧏ x₂
[PROOFSTEP]
rw [lf_congr hx hy, lf_congr hy hx]
[GOAL]
x y : PGame
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y
[PROOFSTEP]
cases' le_or_gf x y with h₁ h₁
[GOAL]
case inl
x y : PGame
h₁ : x ≤ y
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y
[PROOFSTEP]
cases' le_or_gf y x with h₂ h₂
[GOAL]
case inr
x y : PGame
h₁ : y ⧏ x
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y
[PROOFSTEP]
cases' le_or_gf y x with h₂ h₂
[GOAL]
case inl.inl
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y
[PROOFSTEP]
right
[GOAL]
case inl.inl.h
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x ≈ y ∨ y < x ∨ x ‖ y
[PROOFSTEP]
left
[GOAL]
case inl.inl.h.h
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x ≈ y
[PROOFSTEP]
exact ⟨h₁, h₂⟩
[GOAL]
case inl.inr
x y : PGame
h₁ : x ≤ y
h₂ : x ⧏ y
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y
[PROOFSTEP]
left
[GOAL]
case inl.inr.h
x y : PGame
h₁ : x ≤ y
h₂ : x ⧏ y
⊢ x < y
[PROOFSTEP]
exact ⟨h₁, h₂⟩
[GOAL]
case inr.inl
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y
[PROOFSTEP]
right
[GOAL]
case inr.inl.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ x ≈ y ∨ y < x ∨ x ‖ y
[PROOFSTEP]
right
[GOAL]
case inr.inl.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ y < x ∨ x ‖ y
[PROOFSTEP]
left
[GOAL]
case inr.inl.h.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ y < x
[PROOFSTEP]
exact ⟨h₂, h₁⟩
[GOAL]
case inr.inr
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y
[PROOFSTEP]
right
[GOAL]
case inr.inr.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ x ≈ y ∨ y < x ∨ x ‖ y
[PROOFSTEP]
right
[GOAL]
case inr.inr.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ y < x ∨ x ‖ y
[PROOFSTEP]
right
[GOAL]
case inr.inr.h.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ x ‖ y
[PROOFSTEP]
exact ⟨h₂, h₁⟩
[GOAL]
x y : PGame
⊢ x < y ∨ x ≈ y ∨ y ⧏ x
[PROOFSTEP]
rw [lf_iff_lt_or_fuzzy, Fuzzy.swap_iff]
[GOAL]
x y : PGame
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y
[PROOFSTEP]
exact lt_or_equiv_or_gt_or_fuzzy x y
[GOAL]
x y : PGame
L : LeftMoves y ≃ LeftMoves x
R : RightMoves y ≃ RightMoves x
hL : (i : LeftMoves y) → moveLeft x (↑L i) ≡r moveLeft y i
hR : (j : RightMoves y) → moveRight x (↑R j) ≡r moveRight y j
i : LeftMoves x
⊢ moveLeft x i ≡r moveLeft y (↑L.symm i)
[PROOFSTEP]
simpa using hL (L.symm i)
[GOAL]
x y : PGame
L : LeftMoves y ≃ LeftMoves x
R : RightMoves y ≃ RightMoves x
hL : (i : LeftMoves y) → moveLeft x (↑L i) ≡r moveLeft y i
hR : (j : RightMoves y) → moveRight x (↑R j) ≡r moveRight y j
j : RightMoves x
⊢ moveRight x j ≡r moveRight y (↑R.symm j)
[PROOFSTEP]
simpa using hR (R.symm j)
[GOAL]
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hL : (i : LeftMoves x) → PGame.moveLeft x i ≡r PGame.moveLeft y (↑L i)
hR : (j : RightMoves x) → moveRight x j ≡r moveRight y (↑R j)
i : LeftMoves y
⊢ PGame.moveLeft x (↑(leftMovesEquiv (mk L R hL hR)).symm i) ≡r PGame.moveLeft y i
[PROOFSTEP]
simpa using hL (L.symm i)
[GOAL]
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hL : (i : LeftMoves x) → PGame.moveLeft x i ≡r PGame.moveLeft y (↑L i)
hR : (j : RightMoves x) → PGame.moveRight x j ≡r PGame.moveRight y (↑R j)
i : RightMoves y
⊢ PGame.moveRight x (↑(rightMovesEquiv (mk L R hL hR)).symm i) ≡r PGame.moveRight y i
[PROOFSTEP]
simpa using hR (R.symm i)
[GOAL]
x : PGame
xl' xr' : Type u_1
el : xl' ≃ LeftMoves x
er : xr' ≃ RightMoves x
i : LeftMoves x
⊢ moveLeft (relabel el er) (↑el.symm i) = moveLeft x i
[PROOFSTEP]
simp
[GOAL]
x : PGame
xl' xr' : Type u_1
el : xl' ≃ LeftMoves x
er : xr' ≃ RightMoves x
j : RightMoves x
⊢ moveRight (relabel el er) (↑er.symm j) = moveRight x j
[PROOFSTEP]
simp
[GOAL]
x : PGame
xl' xr' : Type ?u.102898
el : xl' ≃ LeftMoves x
er : xr' ≃ RightMoves x
i : LeftMoves (relabel el er)
⊢ moveLeft x (↑el i) ≡r moveLeft (relabel el er) i
[PROOFSTEP]
simp
[GOAL]
x : PGame
xl' xr' : Type ?u.102898
el : xl' ≃ LeftMoves x
er : xr' ≃ RightMoves x
i : LeftMoves (relabel el er)
⊢ moveLeft x (↑el i) ≡r moveLeft x (↑el i)
[PROOFSTEP]
rfl
[GOAL]
x : PGame
xl' xr' : Type ?u.102898
el : xl' ≃ LeftMoves x
er : xr' ≃ RightMoves x
j : RightMoves (relabel el er)
⊢ moveRight x (↑er j) ≡r moveRight (relabel el er) j
[PROOFSTEP]
simp
[GOAL]
x : PGame
xl' xr' : Type ?u.102898
el : xl' ≃ LeftMoves x
er : xr' ≃ RightMoves x
j : RightMoves (relabel el er)
⊢ moveRight x (↑er j) ≡r moveRight x (↑er j)
[PROOFSTEP]
rfl
[GOAL]
src✝ : Neg PGame := inferInstanceAs (Neg PGame)
x : PGame
⊢ - -x = x
[PROOFSTEP]
induction' x with xl xr xL xR ihL ihR
[GOAL]
case mk
src✝ : Neg PGame := inferInstanceAs (Neg PGame)
xl xr : Type ?u.103970
xL : xl → PGame
xR : xr → PGame
ihL : ∀ (a : xl), - -xL a = xL a
ihR : ∀ (a : xr), - -xR a = xR a
⊢ - -mk xl xr xL xR = mk xl xr xL xR
[PROOFSTEP]
simp_rw [neg_def, ihL, ihR]
[GOAL]
src✝¹ : Zero PGame := inferInstanceAs (Zero PGame)
src✝ : Neg PGame := inferInstanceAs (Neg PGame)
⊢ -0 = 0
[PROOFSTEP]
dsimp [Zero.zero, Neg.neg, neg]
[GOAL]
src✝¹ : Zero PGame := inferInstanceAs (Zero PGame)
src✝ : Neg PGame := inferInstanceAs (Neg PGame)
⊢ (mk PEmpty PEmpty (fun i => neg (PEmpty.elim i)) fun i => neg (PEmpty.elim i)) = 0
[PROOFSTEP]
congr
[GOAL]
case e_a
src✝¹ : Zero PGame := inferInstanceAs (Zero PGame)
src✝ : Neg PGame := inferInstanceAs (Neg PGame)
⊢ (fun i => neg (PEmpty.elim i)) = PEmpty.elim
[PROOFSTEP]
funext i
[GOAL]
case e_a
src✝¹ : Zero PGame := inferInstanceAs (Zero PGame)
src✝ : Neg PGame := inferInstanceAs (Neg PGame)
⊢ (fun i => neg (PEmpty.elim i)) = PEmpty.elim
[PROOFSTEP]
funext i
[GOAL]
case e_a.h
src✝¹ : Zero PGame := inferInstanceAs (Zero PGame)
src✝ : Neg PGame := inferInstanceAs (Neg PGame)
i : PEmpty
⊢ neg (PEmpty.elim i) = PEmpty.elim i
[PROOFSTEP]
cases i
[GOAL]
case e_a.h
src✝¹ : Zero PGame := inferInstanceAs (Zero PGame)
src✝ : Neg PGame := inferInstanceAs (Neg PGame)
i : PEmpty
⊢ neg (PEmpty.elim i) = PEmpty.elim i
[PROOFSTEP]
cases i
[GOAL]
L R : List PGame
⊢ -ofLists L R = ofLists (List.map (fun x => -x) R) (List.map (fun x => -x) L)
[PROOFSTEP]
set_option linter.deprecated
  false in
  simp only [ofLists, neg_def, List.length_map, List.nthLe_map', eq_self_iff_true, true_and, mk.injEq]
  constructor
  all_goals
    apply hfunext
    · simp
    · intro a a' ha
      congr 2
      have : ∀ {m n} (_ : m = n) {b : ULift (Fin m)} {c : ULift (Fin n)} (_ : HEq b c), (b.down : ℕ) = ↑c.down :=
        by
        rintro m n rfl b c
        simp only [heq_eq_eq]
        rintro rfl
        rfl
      exact this (List.length_map _ _).symm ha
[GOAL]
L R : List PGame
⊢ -ofLists L R = ofLists (List.map (fun x => -x) R) (List.map (fun x => -x) L)
[PROOFSTEP]
simp only [ofLists, neg_def, List.length_map, List.nthLe_map', eq_self_iff_true, true_and, mk.injEq]
[GOAL]
L R : List PGame
⊢ (HEq (fun j => -List.nthLe R ↑j.down (_ : ↑j.down < List.length R)) fun i =>
      -List.nthLe R ↑i.down (_ : ↑i.down < List.length R)) ∧
    HEq (fun i => -List.nthLe L ↑i.down (_ : ↑i.down < List.length L)) fun j =>
      -List.nthLe L ↑j.down (_ : ↑j.down < List.length L)
[PROOFSTEP]
constructor
[GOAL]
case left
L R : List PGame
⊢ HEq (fun j => -List.nthLe R ↑j.down (_ : ↑j.down < List.length R)) fun i =>
    -List.nthLe R ↑i.down (_ : ↑i.down < List.length R)
case right
L R : List PGame
⊢ HEq (fun i => -List.nthLe L ↑i.down (_ : ↑i.down < List.length L)) fun j =>
    -List.nthLe L ↑j.down (_ : ↑j.down < List.length L)
[PROOFSTEP]
all_goals
  apply hfunext
  · simp
  · intro a a' ha
    congr 2
    have : ∀ {m n} (_ : m = n) {b : ULift (Fin m)} {c : ULift (Fin n)} (_ : HEq b c), (b.down : ℕ) = ↑c.down :=
      by
      rintro m n rfl b c
      simp only [heq_eq_eq]
      rintro rfl
      rfl
    exact this (List.length_map _ _).symm ha
[GOAL]
case left
L R : List PGame
⊢ HEq (fun j => -List.nthLe R ↑j.down (_ : ↑j.down < List.length R)) fun i =>
    -List.nthLe R ↑i.down (_ : ↑i.down < List.length R)
[PROOFSTEP]
apply hfunext
[GOAL]
case left.hα
L R : List PGame
⊢ ULift (Fin (List.length R)) = ULift (Fin (List.length (List.map (fun x => -x) R)))
[PROOFSTEP]
simp
[GOAL]
case left.h
L R : List PGame
⊢ ∀ (a : ULift (Fin (List.length R))) (a' : ULift (Fin (List.length (List.map (fun x => -x) R)))),
    HEq a a' →
      HEq (-List.nthLe R ↑a.down (_ : ↑a.down < List.length R)) (-List.nthLe R ↑a'.down (_ : ↑a'.down < List.length R))
[PROOFSTEP]
intro a a' ha
[GOAL]
case left.h
L R : List PGame
a : ULift (Fin (List.length R))
a' : ULift (Fin (List.length (List.map (fun x => -x) R)))
ha : HEq a a'
⊢ HEq (-List.nthLe R ↑a.down (_ : ↑a.down < List.length R)) (-List.nthLe R ↑a'.down (_ : ↑a'.down < List.length R))
[PROOFSTEP]
congr 2
[GOAL]
case left.h.h.e_a.e_n
L R : List PGame
a : ULift (Fin (List.length R))
a' : ULift (Fin (List.length (List.map (fun x => -x) R)))
ha : HEq a a'
⊢ ↑a.down = ↑a'.down
[PROOFSTEP]
have : ∀ {m n} (_ : m = n) {b : ULift (Fin m)} {c : ULift (Fin n)} (_ : HEq b c), (b.down : ℕ) = ↑c.down :=
  by
  rintro m n rfl b c
  simp only [heq_eq_eq]
  rintro rfl
  rfl
[GOAL]
L R : List PGame
a : ULift (Fin (List.length R))
a' : ULift (Fin (List.length (List.map (fun x => -x) R)))
ha : HEq a a'
⊢ ∀ {m n : ℕ}, m = n → ∀ {b : ULift (Fin m)} {c : ULift (Fin n)}, HEq b c → ↑b.down = ↑c.down
[PROOFSTEP]
rintro m n rfl b c
[GOAL]
L R : List PGame
a : ULift (Fin (List.length R))
a' : ULift (Fin (List.length (List.map (fun x => -x) R)))
ha : HEq a a'
m : ℕ
b c : ULift (Fin m)
⊢ HEq b c → ↑b.down = ↑c.down
[PROOFSTEP]
simp only [heq_eq_eq]
[GOAL]
L R : List PGame
a : ULift (Fin (List.length R))
a' : ULift (Fin (List.length (List.map (fun x => -x) R)))
ha : HEq a a'
m : ℕ
b c : ULift (Fin m)
⊢ b = c → ↑b.down = ↑c.down
[PROOFSTEP]
rintro rfl
[GOAL]
L R : List PGame
a : ULift (Fin (List.length R))
a' : ULift (Fin (List.length (List.map (fun x => -x) R)))
ha : HEq a a'
m : ℕ
b : ULift (Fin m)
⊢ ↑b.down = ↑b.down
[PROOFSTEP]
rfl
[GOAL]
case left.h.h.e_a.e_n
L R : List PGame
a : ULift (Fin (List.length R))
a' : ULift (Fin (List.length (List.map (fun x => -x) R)))
ha : HEq a a'
this : ∀ {m n : ℕ}, m = n → ∀ {b : ULift (Fin m)} {c : ULift (Fin n)}, HEq b c → ↑b.down = ↑c.down
⊢ ↑a.down = ↑a'.down
[PROOFSTEP]
exact this (List.length_map _ _).symm ha
[GOAL]
case right
L R : List PGame
⊢ HEq (fun i => -List.nthLe L ↑i.down (_ : ↑i.down < List.length L)) fun j =>
    -List.nthLe L ↑j.down (_ : ↑j.down < List.length L)
[PROOFSTEP]
apply hfunext
[GOAL]
case right.hα
L R : List PGame
⊢ ULift (Fin (List.length L)) = ULift (Fin (List.length (List.map (fun x => -x) L)))
[PROOFSTEP]
simp
[GOAL]
case right.h
L R : List PGame
⊢ ∀ (a : ULift (Fin (List.length L))) (a' : ULift (Fin (List.length (List.map (fun x => -x) L)))),
    HEq a a' →
      HEq (-List.nthLe L ↑a.down (_ : ↑a.down < List.length L)) (-List.nthLe L ↑a'.down (_ : ↑a'.down < List.length L))
[PROOFSTEP]
intro a a' ha
[GOAL]
case right.h
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
⊢ HEq (-List.nthLe L ↑a.down (_ : ↑a.down < List.length L)) (-List.nthLe L ↑a'.down (_ : ↑a'.down < List.length L))
[PROOFSTEP]
congr 2
[GOAL]
case right.h.h.e_a.e_n
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
⊢ ↑a.down = ↑a'.down
[PROOFSTEP]
have : ∀ {m n} (_ : m = n) {b : ULift (Fin m)} {c : ULift (Fin n)} (_ : HEq b c), (b.down : ℕ) = ↑c.down :=
  by
  rintro m n rfl b c
  simp only [heq_eq_eq]
  rintro rfl
  rfl
[GOAL]
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
⊢ ∀ {m n : ℕ}, m = n → ∀ {b : ULift (Fin m)} {c : ULift (Fin n)}, HEq b c → ↑b.down = ↑c.down
[PROOFSTEP]
rintro m n rfl b c
[GOAL]
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
m : ℕ
b c : ULift (Fin m)
⊢ HEq b c → ↑b.down = ↑c.down
[PROOFSTEP]
simp only [heq_eq_eq]
[GOAL]
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
m : ℕ
b c : ULift (Fin m)
⊢ b = c → ↑b.down = ↑c.down
[PROOFSTEP]
rintro rfl
[GOAL]
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
m : ℕ
b : ULift (Fin m)
⊢ ↑b.down = ↑b.down
[PROOFSTEP]
rfl
[GOAL]
case right.h.h.e_a.e_n
L R : List PGame
a : ULift (Fin (List.length L))
a' : ULift (Fin (List.length (List.map (fun x => -x) L)))
ha : HEq a a'
this : ∀ {m n : ℕ}, m = n → ∀ {b : ULift (Fin m)} {c : ULift (Fin n)}, HEq b c → ↑b.down = ↑c.down
⊢ ↑a.down = ↑a'.down
[PROOFSTEP]
exact this (List.length_map _ _).symm ha
[GOAL]
x y : PGame
⊢ IsOption x (-y) ↔ IsOption (-x) y
[PROOFSTEP]
rw [IsOption_iff, IsOption_iff, or_comm]
[GOAL]
x y : PGame
⊢ ((∃ i, x = moveRight (-y) i) ∨ ∃ i, x = moveLeft (-y) i) ↔ (∃ i, -x = moveLeft y i) ∨ ∃ i, -x = moveRight y i
[PROOFSTEP]
cases y
[GOAL]
case mk
x : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ((∃ i, x = moveRight (-mk α✝ β✝ a✝¹ a✝) i) ∨ ∃ i, x = moveLeft (-mk α✝ β✝ a✝¹ a✝) i) ↔
    (∃ i, -x = moveLeft (mk α✝ β✝ a✝¹ a✝) i) ∨ ∃ i, -x = moveRight (mk α✝ β✝ a✝¹ a✝) i
[PROOFSTEP]
apply or_congr
[GOAL]
case mk.h₁
x : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (∃ i, x = moveRight (-mk α✝ β✝ a✝¹ a✝) i) ↔ ∃ i, -x = moveLeft (mk α✝ β✝ a✝¹ a✝) i
[PROOFSTEP]
apply exists_congr
[GOAL]
case mk.h₁.h
x : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ∀ (a : RightMoves (-mk α✝ β✝ a✝¹ a✝)), x = moveRight (-mk α✝ β✝ a✝¹ a✝) a ↔ -x = moveLeft (mk α✝ β✝ a✝¹ a✝) a
[PROOFSTEP]
intro
[GOAL]
case mk.h₁.h
x : PGame
α✝ β✝ : Type u_1
a✝² : α✝ → PGame
a✝¹ : β✝ → PGame
a✝ : RightMoves (-mk α✝ β✝ a✝² a✝¹)
⊢ x = moveRight (-mk α✝ β✝ a✝² a✝¹) a✝ ↔ -x = moveLeft (mk α✝ β✝ a✝² a✝¹) a✝
[PROOFSTEP]
rw [neg_eq_iff_eq_neg]
[GOAL]
case mk.h₁.h
x : PGame
α✝ β✝ : Type u_1
a✝² : α✝ → PGame
a✝¹ : β✝ → PGame
a✝ : RightMoves (-mk α✝ β✝ a✝² a✝¹)
⊢ x = moveRight (-mk α✝ β✝ a✝² a✝¹) a✝ ↔ x = -moveLeft (mk α✝ β✝ a✝² a✝¹) a✝
[PROOFSTEP]
rfl
[GOAL]
case mk.h₂
x : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (∃ i, x = moveLeft (-mk α✝ β✝ a✝¹ a✝) i) ↔ ∃ i, -x = moveRight (mk α✝ β✝ a✝¹ a✝) i
[PROOFSTEP]
apply exists_congr
[GOAL]
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ∀ (a : LeftMoves (-mk α✝ β✝ a✝¹ a✝)), x = moveLeft (-mk α✝ β✝ a✝¹ a✝) a ↔ -x = moveRight (mk α✝ β✝ a✝¹ a✝) a
[PROOFSTEP]
intro
[GOAL]
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝² : α✝ → PGame
a✝¹ : β✝ → PGame
a✝ : LeftMoves (-mk α✝ β✝ a✝² a✝¹)
⊢ x = moveLeft (-mk α✝ β✝ a✝² a✝¹) a✝ ↔ -x = moveRight (mk α✝ β✝ a✝² a✝¹) a✝
[PROOFSTEP]
rw [neg_eq_iff_eq_neg]
[GOAL]
case mk.h₂.h
x : PGame
α✝ β✝ : Type u_1
a✝² : α✝ → PGame
a✝¹ : β✝ → PGame
a✝ : LeftMoves (-mk α✝ β✝ a✝² a✝¹)
⊢ x = moveLeft (-mk α✝ β✝ a✝² a✝¹) a✝ ↔ x = -moveRight (mk α✝ β✝ a✝² a✝¹) a✝
[PROOFSTEP]
rfl
[GOAL]
x y : PGame
⊢ IsOption (-x) (-y) ↔ IsOption x y
[PROOFSTEP]
rw [isOption_neg, neg_neg]
[GOAL]
x : PGame
i : RightMoves x
⊢ moveLeft (-x) (↑toLeftMovesNeg i) = -moveRight x i
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : RightMoves (mk α✝ β✝ a✝¹ a✝)
⊢ moveLeft (-mk α✝ β✝ a✝¹ a✝) (↑toLeftMovesNeg i) = -moveRight (mk α✝ β✝ a✝¹ a✝) i
[PROOFSTEP]
rfl
[GOAL]
x : PGame
i : LeftMoves (-x)
⊢ moveLeft (-x) i = -moveRight x (↑toLeftMovesNeg.symm i)
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : LeftMoves (-mk α✝ β✝ a✝¹ a✝)
⊢ moveLeft (-mk α✝ β✝ a✝¹ a✝) i = -moveRight (mk α✝ β✝ a✝¹ a✝) (↑toLeftMovesNeg.symm i)
[PROOFSTEP]
rfl
[GOAL]
x : PGame
i : LeftMoves x
⊢ moveRight (-x) (↑toRightMovesNeg i) = -moveLeft x i
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : LeftMoves (mk α✝ β✝ a✝¹ a✝)
⊢ moveRight (-mk α✝ β✝ a✝¹ a✝) (↑toRightMovesNeg i) = -moveLeft (mk α✝ β✝ a✝¹ a✝) i
[PROOFSTEP]
rfl
[GOAL]
x : PGame
i : RightMoves (-x)
⊢ moveRight (-x) i = -moveLeft x (↑toRightMovesNeg.symm i)
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : RightMoves (-mk α✝ β✝ a✝¹ a✝)
⊢ moveRight (-mk α✝ β✝ a✝¹ a✝) i = -moveLeft (mk α✝ β✝ a✝¹ a✝) (↑toRightMovesNeg.symm i)
[PROOFSTEP]
rfl
[GOAL]
x : PGame
i : RightMoves (-x)
⊢ moveLeft x (↑toRightMovesNeg.symm i) = -moveRight (-x) i
[PROOFSTEP]
simp
[GOAL]
x : PGame
i : LeftMoves x
⊢ moveLeft x i = -moveRight (-x) (↑toRightMovesNeg i)
[PROOFSTEP]
simp
[GOAL]
x : PGame
i : LeftMoves (-x)
⊢ moveRight x (↑toLeftMovesNeg.symm i) = -moveLeft (-x) i
[PROOFSTEP]
simp
[GOAL]
x : PGame
i : RightMoves x
⊢ moveRight x i = -moveLeft (-x) (↑toLeftMovesNeg i)
[PROOFSTEP]
simp
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (-mk yl yr yL yR ≤ -mk xl xr xL xR ↔ mk xl xr xL xR ≤ mk yl yr yL yR) ∧
    (-mk yl yr yL yR ⧏ -mk xl xr xL xR ↔ mk xl xr xL xR ⧏ mk yl yr yL yR)
[PROOFSTEP]
simp_rw [neg_def, mk_le_mk, mk_lf_mk, ← neg_def]
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (((∀ (i : yr), -yR i ⧏ -mk xl xr (fun i => xL i) fun j => xR j) ∧
        ∀ (j : xl), (-mk yl yr (fun i => yL i) fun j => yR j) ⧏ -xL j) ↔
      (∀ (i : xl), xL i ⧏ mk yl yr yL yR) ∧ ∀ (j : yr), mk xl xr xL xR ⧏ yR j) ∧
    (((∃ i, (-mk yl yr (fun i => yL i) fun j => yR j) ≤ -xR i) ∨ ∃ j, -yL j ≤ -mk xl xr (fun i => xL i) fun j => xR j) ↔
      (∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR)
[PROOFSTEP]
constructor
[GOAL]
case left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((∀ (i : yr), -yR i ⧏ -mk xl xr (fun i => xL i) fun j => xR j) ∧
      ∀ (j : xl), (-mk yl yr (fun i => yL i) fun j => yR j) ⧏ -xL j) ↔
    (∀ (i : xl), xL i ⧏ mk yl yr yL yR) ∧ ∀ (j : yr), mk xl xr xL xR ⧏ yR j
[PROOFSTEP]
rw [and_comm]
[GOAL]
case left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((∀ (j : xl), (-mk yl yr (fun i => yL i) fun j => yR j) ⧏ -xL j) ∧
      ∀ (i : yr), -yR i ⧏ -mk xl xr (fun i => xL i) fun j => xR j) ↔
    (∀ (i : xl), xL i ⧏ mk yl yr yL yR) ∧ ∀ (j : yr), mk xl xr xL xR ⧏ yR j
[PROOFSTEP]
apply and_congr
[GOAL]
case left.h₁
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (∀ (j : xl), (-mk yl yr (fun i => yL i) fun j => yR j) ⧏ -xL j) ↔ ∀ (i : xl), xL i ⧏ mk yl yr yL yR
[PROOFSTEP]
exact forall_congr' fun _ => neg_le_lf_neg_iff.2
[GOAL]
case left.h₂
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (∀ (i : yr), -yR i ⧏ -mk xl xr (fun i => xL i) fun j => xR j) ↔ ∀ (j : yr), mk xl xr xL xR ⧏ yR j
[PROOFSTEP]
exact forall_congr' fun _ => neg_le_lf_neg_iff.2
[GOAL]
case right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((∃ i, (-mk yl yr (fun i => yL i) fun j => yR j) ≤ -xR i) ∨ ∃ j, -yL j ≤ -mk xl xr (fun i => xL i) fun j => xR j) ↔
    (∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR
[PROOFSTEP]
rw [or_comm]
[GOAL]
case right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((∃ j, -yL j ≤ -mk xl xr (fun i => xL i) fun j => xR j) ∨ ∃ i, (-mk yl yr (fun i => yL i) fun j => yR j) ≤ -xR i) ↔
    (∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR
[PROOFSTEP]
apply or_congr
[GOAL]
case right.h₁
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (∃ j, -yL j ≤ -mk xl xr (fun i => xL i) fun j => xR j) ↔ ∃ i, mk xl xr xL xR ≤ yL i
[PROOFSTEP]
exact exists_congr fun _ => neg_le_lf_neg_iff.1
[GOAL]
case right.h₂
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (∃ i, (-mk yl yr (fun i => yL i) fun j => yR j) ≤ -xR i) ↔ ∃ j, xR j ≤ mk yl yr yL yR
[PROOFSTEP]
exact exists_congr fun _ => neg_le_lf_neg_iff.1
[GOAL]
x y : PGame
⊢ -y < -x ↔ x < y
[PROOFSTEP]
rw [lt_iff_le_and_lf, lt_iff_le_and_lf, neg_le_neg_iff, neg_lf_neg_iff]
[GOAL]
x y : PGame
⊢ -x ≈ -y ↔ x ≈ y
[PROOFSTEP]
show Equiv (-x) (-y) ↔ Equiv x y
[GOAL]
x y : PGame
⊢ Equiv (-x) (-y) ↔ Equiv x y
[PROOFSTEP]
rw [Equiv, Equiv, neg_le_neg_iff, neg_le_neg_iff, and_comm]
[GOAL]
x y : PGame
⊢ -x ‖ -y ↔ x ‖ y
[PROOFSTEP]
rw [Fuzzy, Fuzzy, neg_lf_neg_iff, neg_lf_neg_iff, and_comm]
[GOAL]
x y : PGame
⊢ -y ≤ x ↔ -x ≤ y
[PROOFSTEP]
rw [← neg_neg x, neg_le_neg_iff, neg_neg]
[GOAL]
x y : PGame
⊢ -y ⧏ x ↔ -x ⧏ y
[PROOFSTEP]
rw [← neg_neg x, neg_lf_neg_iff, neg_neg]
[GOAL]
x y : PGame
⊢ -y < x ↔ -x < y
[PROOFSTEP]
rw [← neg_neg x, neg_lt_neg_iff, neg_neg]
[GOAL]
x y : PGame
⊢ -x ≈ y ↔ x ≈ -y
[PROOFSTEP]
rw [← neg_neg y, neg_equiv_neg_iff, neg_neg]
[GOAL]
x y : PGame
⊢ -x ‖ y ↔ x ‖ -y
[PROOFSTEP]
rw [← neg_neg y, neg_fuzzy_neg_iff, neg_neg]
[GOAL]
x y : PGame
⊢ y ≤ -x ↔ x ≤ -y
[PROOFSTEP]
rw [← neg_neg x, neg_le_neg_iff, neg_neg]
[GOAL]
x y : PGame
⊢ y ⧏ -x ↔ x ⧏ -y
[PROOFSTEP]
rw [← neg_neg x, neg_lf_neg_iff, neg_neg]
[GOAL]
x y : PGame
⊢ y < -x ↔ x < -y
[PROOFSTEP]
rw [← neg_neg x, neg_lt_neg_iff, neg_neg]
[GOAL]
x : PGame
⊢ -x ≤ 0 ↔ 0 ≤ x
[PROOFSTEP]
rw [neg_le_iff, neg_zero]
[GOAL]
x : PGame
⊢ 0 ≤ -x ↔ x ≤ 0
[PROOFSTEP]
rw [le_neg_iff, neg_zero]
[GOAL]
x : PGame
⊢ -x ⧏ 0 ↔ 0 ⧏ x
[PROOFSTEP]
rw [neg_lf_iff, neg_zero]
[GOAL]
x : PGame
⊢ 0 ⧏ -x ↔ x ⧏ 0
[PROOFSTEP]
rw [lf_neg_iff, neg_zero]
[GOAL]
x : PGame
⊢ -x < 0 ↔ 0 < x
[PROOFSTEP]
rw [neg_lt_iff, neg_zero]
[GOAL]
x : PGame
⊢ 0 < -x ↔ x < 0
[PROOFSTEP]
rw [lt_neg_iff, neg_zero]
[GOAL]
x : PGame
⊢ -x ≈ 0 ↔ x ≈ 0
[PROOFSTEP]
rw [neg_equiv_iff, neg_zero]
[GOAL]
x : PGame
⊢ -x ‖ 0 ↔ x ‖ 0
[PROOFSTEP]
rw [neg_fuzzy_iff, neg_zero]
[GOAL]
x : PGame
⊢ 0 ≈ -x ↔ 0 ≈ x
[PROOFSTEP]
rw [← neg_equiv_iff, neg_zero]
[GOAL]
x : PGame
⊢ 0 ‖ -x ↔ 0 ‖ x
[PROOFSTEP]
rw [← neg_fuzzy_iff, neg_zero]
[GOAL]
x y : PGame
⊢ PGame
[PROOFSTEP]
induction' x with xl xr _ _ IHxl IHxr generalizing y
[GOAL]
case mk
y✝ : PGame
xl xr : Type u
a✝¹ : xl → PGame
a✝ : xr → PGame
IHxl : xl → PGame → PGame
IHxr : xr → PGame → PGame
y : PGame
⊢ PGame
[PROOFSTEP]
induction' y with yl yr yL yR IHyl IHyr
[GOAL]
case mk.mk
y : PGame
xl xr : Type u
a✝¹ : xl → PGame
a✝ : xr → PGame
IHxl : xl → PGame → PGame
IHxr : xr → PGame → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
IHyl : yl → PGame
IHyr : yr → PGame
⊢ PGame
[PROOFSTEP]
have y := mk yl yr yL yR
[GOAL]
case mk.mk
y✝ : PGame
xl xr : Type u
a✝¹ : xl → PGame
a✝ : xr → PGame
IHxl : xl → PGame → PGame
IHxr : xr → PGame → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
IHyl : yl → PGame
IHyr : yr → PGame
y : PGame
⊢ PGame
[PROOFSTEP]
refine' ⟨Sum xl yl, Sum xr yr, Sum.rec _ _, Sum.rec _ _⟩
[GOAL]
case mk.mk.refine'_1
y✝ : PGame
xl xr : Type u
a✝¹ : xl → PGame
a✝ : xr → PGame
IHxl : xl → PGame → PGame
IHxr : xr → PGame → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
IHyl : yl → PGame
IHyr : yr → PGame
y : PGame
⊢ xl → PGame
[PROOFSTEP]
exact fun i => IHxl i y
[GOAL]
case mk.mk.refine'_2
y✝ : PGame
xl xr : Type u
a✝¹ : xl → PGame
a✝ : xr → PGame
IHxl : xl → PGame → PGame
IHxr : xr → PGame → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
IHyl : yl → PGame
IHyr : yr → PGame
y : PGame
⊢ yl → PGame
[PROOFSTEP]
exact IHyl
[GOAL]
case mk.mk.refine'_3
y✝ : PGame
xl xr : Type u
a✝¹ : xl → PGame
a✝ : xr → PGame
IHxl : xl → PGame → PGame
IHxr : xr → PGame → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
IHyl : yl → PGame
IHyr : yr → PGame
y : PGame
⊢ xr → PGame
[PROOFSTEP]
exact fun i => IHxr i y
[GOAL]
case mk.mk.refine'_4
y✝ : PGame
xl xr : Type u
a✝¹ : xl → PGame
a✝ : xr → PGame
IHxl : xl → PGame → PGame
IHxr : xr → PGame → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
IHyl : yl → PGame
IHyr : yr → PGame
y : PGame
⊢ yr → PGame
[PROOFSTEP]
exact IHyr
[GOAL]
x y : PGame
inst✝¹ : IsEmpty (LeftMoves x)
inst✝ : IsEmpty (LeftMoves y)
⊢ IsEmpty (LeftMoves (x + y))
[PROOFSTEP]
cases x
[GOAL]
case mk
y : PGame
inst✝¹ : IsEmpty (LeftMoves y)
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
inst✝ : IsEmpty (LeftMoves (mk α✝ β✝ a✝¹ a✝))
⊢ IsEmpty (LeftMoves (mk α✝ β✝ a✝¹ a✝ + y))
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
α✝¹ β✝¹ : Type u
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
inst✝¹ : IsEmpty (LeftMoves (mk α✝¹ β✝¹ a✝³ a✝²))
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
inst✝ : IsEmpty (LeftMoves (mk α✝ β✝ a✝¹ a✝))
⊢ IsEmpty (LeftMoves (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝))
[PROOFSTEP]
apply isEmpty_sum.2 ⟨_, _⟩
[GOAL]
α✝¹ β✝¹ : Type u
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
inst✝¹ : IsEmpty (LeftMoves (mk α✝¹ β✝¹ a✝³ a✝²))
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
inst✝ : IsEmpty (LeftMoves (mk α✝ β✝ a✝¹ a✝))
⊢ IsEmpty α✝¹
α✝¹ β✝¹ : Type u
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
inst✝¹ : IsEmpty (LeftMoves (mk α✝¹ β✝¹ a✝³ a✝²))
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
inst✝ : IsEmpty (LeftMoves (mk α✝ β✝ a✝¹ a✝))
⊢ IsEmpty α✝
[PROOFSTEP]
assumption'
[GOAL]
x y : PGame
inst✝¹ : IsEmpty (RightMoves x)
inst✝ : IsEmpty (RightMoves y)
⊢ IsEmpty (RightMoves (x + y))
[PROOFSTEP]
cases x
[GOAL]
case mk
y : PGame
inst✝¹ : IsEmpty (RightMoves y)
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
inst✝ : IsEmpty (RightMoves (mk α✝ β✝ a✝¹ a✝))
⊢ IsEmpty (RightMoves (mk α✝ β✝ a✝¹ a✝ + y))
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
α✝¹ β✝¹ : Type u
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
inst✝¹ : IsEmpty (RightMoves (mk α✝¹ β✝¹ a✝³ a✝²))
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
inst✝ : IsEmpty (RightMoves (mk α✝ β✝ a✝¹ a✝))
⊢ IsEmpty (RightMoves (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝))
[PROOFSTEP]
apply isEmpty_sum.2 ⟨_, _⟩
[GOAL]
α✝¹ β✝¹ : Type u
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
inst✝¹ : IsEmpty (RightMoves (mk α✝¹ β✝¹ a✝³ a✝²))
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
inst✝ : IsEmpty (RightMoves (mk α✝ β✝ a✝¹ a✝))
⊢ IsEmpty β✝¹
α✝¹ β✝¹ : Type u
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
inst✝¹ : IsEmpty (RightMoves (mk α✝¹ β✝¹ a✝³ a✝²))
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
inst✝ : IsEmpty (RightMoves (mk α✝ β✝ a✝¹ a✝))
⊢ IsEmpty β✝
[PROOFSTEP]
assumption'
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
⊢ mk xl xr xL xR + 0 ≡r mk xl xr xL xR
[PROOFSTEP]
refine' ⟨Equiv.sumEmpty xl PEmpty, Equiv.sumEmpty xr PEmpty, _, _⟩
[GOAL]
case refine'_1
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
⊢ (i : LeftMoves (mk xl xr xL xR + 0)) →
    moveLeft (mk xl xr xL xR + 0) i ≡r moveLeft (mk xl xr xL xR) (↑(Equiv.sumEmpty xl PEmpty) i)
[PROOFSTEP]
rintro (⟨i⟩ | ⟨⟨⟩⟩)
[GOAL]
case refine'_2
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
⊢ (j : RightMoves (mk xl xr xL xR + 0)) →
    moveRight (mk xl xr xL xR + 0) j ≡r moveRight (mk xl xr xL xR) (↑(Equiv.sumEmpty xr PEmpty) j)
[PROOFSTEP]
rintro (⟨i⟩ | ⟨⟨⟩⟩)
[GOAL]
case refine'_1.inl
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ moveLeft (mk xl xr xL xR + 0) (Sum.inl i) ≡r moveLeft (mk xl xr xL xR) (↑(Equiv.sumEmpty xl PEmpty) (Sum.inl i))
[PROOFSTEP]
apply addZeroRelabelling
[GOAL]
case refine'_2.inl
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ moveRight (mk xl xr xL xR + 0) (Sum.inl i) ≡r moveRight (mk xl xr xL xR) (↑(Equiv.sumEmpty xr PEmpty) (Sum.inl i))
[PROOFSTEP]
apply addZeroRelabelling
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
⊢ 0 + mk xl xr xL xR ≡r mk xl xr xL xR
[PROOFSTEP]
refine' ⟨Equiv.emptySum PEmpty xl, Equiv.emptySum PEmpty xr, _, _⟩
[GOAL]
case refine'_1
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
⊢ (i : LeftMoves (0 + mk xl xr xL xR)) →
    moveLeft (0 + mk xl xr xL xR) i ≡r moveLeft (mk xl xr xL xR) (↑(Equiv.emptySum PEmpty xl) i)
[PROOFSTEP]
rintro (⟨⟨⟩⟩ | ⟨i⟩)
[GOAL]
case refine'_2
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
⊢ (j : RightMoves (0 + mk xl xr xL xR)) →
    moveRight (0 + mk xl xr xL xR) j ≡r moveRight (mk xl xr xL xR) (↑(Equiv.emptySum PEmpty xr) j)
[PROOFSTEP]
rintro (⟨⟨⟩⟩ | ⟨i⟩)
[GOAL]
case refine'_1.inr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ moveLeft (0 + mk xl xr xL xR) (Sum.inr i) ≡r moveLeft (mk xl xr xL xR) (↑(Equiv.emptySum PEmpty xl) (Sum.inr i))
[PROOFSTEP]
apply zeroAddRelabelling
[GOAL]
case refine'_2.inr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ moveRight (0 + mk xl xr xL xR) (Sum.inr i) ≡r moveRight (mk xl xr xL xR) (↑(Equiv.emptySum PEmpty xr) (Sum.inr i))
[PROOFSTEP]
apply zeroAddRelabelling
[GOAL]
x y : PGame
i : LeftMoves x
⊢ moveLeft (x + y) (↑toLeftMovesAdd (Sum.inl i)) = moveLeft x i + y
[PROOFSTEP]
cases x
[GOAL]
case mk
y : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : LeftMoves (mk α✝ β✝ a✝¹ a✝)
⊢ moveLeft (mk α✝ β✝ a✝¹ a✝ + y) (↑toLeftMovesAdd (Sum.inl i)) = moveLeft (mk α✝ β✝ a✝¹ a✝) i + y
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : LeftMoves (mk α✝¹ β✝¹ a✝³ a✝²)
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ moveLeft (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝) (↑toLeftMovesAdd (Sum.inl i)) =
    moveLeft (mk α✝¹ β✝¹ a✝³ a✝²) i + mk α✝ β✝ a✝¹ a✝
[PROOFSTEP]
rfl
[GOAL]
x y : PGame
i : RightMoves x
⊢ moveRight (x + y) (↑toRightMovesAdd (Sum.inl i)) = moveRight x i + y
[PROOFSTEP]
cases x
[GOAL]
case mk
y : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : RightMoves (mk α✝ β✝ a✝¹ a✝)
⊢ moveRight (mk α✝ β✝ a✝¹ a✝ + y) (↑toRightMovesAdd (Sum.inl i)) = moveRight (mk α✝ β✝ a✝¹ a✝) i + y
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : RightMoves (mk α✝¹ β✝¹ a✝³ a✝²)
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ moveRight (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝) (↑toRightMovesAdd (Sum.inl i)) =
    moveRight (mk α✝¹ β✝¹ a✝³ a✝²) i + mk α✝ β✝ a✝¹ a✝
[PROOFSTEP]
rfl
[GOAL]
x y : PGame
i : LeftMoves y
⊢ moveLeft (x + y) (↑toLeftMovesAdd (Sum.inr i)) = x + moveLeft y i
[PROOFSTEP]
cases x
[GOAL]
case mk
y : PGame
i : LeftMoves y
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ moveLeft (mk α✝ β✝ a✝¹ a✝ + y) (↑toLeftMovesAdd (Sum.inr i)) = mk α✝ β✝ a✝¹ a✝ + moveLeft y i
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : LeftMoves (mk α✝ β✝ a✝¹ a✝)
⊢ moveLeft (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝) (↑toLeftMovesAdd (Sum.inr i)) =
    mk α✝¹ β✝¹ a✝³ a✝² + moveLeft (mk α✝ β✝ a✝¹ a✝) i
[PROOFSTEP]
rfl
[GOAL]
x y : PGame
i : RightMoves y
⊢ moveRight (x + y) (↑toRightMovesAdd (Sum.inr i)) = x + moveRight y i
[PROOFSTEP]
cases x
[GOAL]
case mk
y : PGame
i : RightMoves y
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ moveRight (mk α✝ β✝ a✝¹ a✝ + y) (↑toRightMovesAdd (Sum.inr i)) = mk α✝ β✝ a✝¹ a✝ + moveRight y i
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : RightMoves (mk α✝ β✝ a✝¹ a✝)
⊢ moveRight (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝) (↑toRightMovesAdd (Sum.inr i)) =
    mk α✝¹ β✝¹ a✝³ a✝² + moveRight (mk α✝ β✝ a✝¹ a✝) i
[PROOFSTEP]
rfl
[GOAL]
x y : PGame
k : LeftMoves (x + y)
P : LeftMoves (x + y) → Prop
hl : ∀ (i : LeftMoves x), P (↑toLeftMovesAdd (Sum.inl i))
hr : ∀ (i : LeftMoves y), P (↑toLeftMovesAdd (Sum.inr i))
⊢ P k
[PROOFSTEP]
rw [← toLeftMovesAdd.apply_symm_apply k]
[GOAL]
x y : PGame
k : LeftMoves (x + y)
P : LeftMoves (x + y) → Prop
hl : ∀ (i : LeftMoves x), P (↑toLeftMovesAdd (Sum.inl i))
hr : ∀ (i : LeftMoves y), P (↑toLeftMovesAdd (Sum.inr i))
⊢ P (↑toLeftMovesAdd (↑toLeftMovesAdd.symm k))
[PROOFSTEP]
cases' toLeftMovesAdd.symm k with i i
[GOAL]
case inl
x y : PGame
k : LeftMoves (x + y)
P : LeftMoves (x + y) → Prop
hl : ∀ (i : LeftMoves x), P (↑toLeftMovesAdd (Sum.inl i))
hr : ∀ (i : LeftMoves y), P (↑toLeftMovesAdd (Sum.inr i))
i : LeftMoves x
⊢ P (↑toLeftMovesAdd (Sum.inl i))
[PROOFSTEP]
exact hl i
[GOAL]
case inr
x y : PGame
k : LeftMoves (x + y)
P : LeftMoves (x + y) → Prop
hl : ∀ (i : LeftMoves x), P (↑toLeftMovesAdd (Sum.inl i))
hr : ∀ (i : LeftMoves y), P (↑toLeftMovesAdd (Sum.inr i))
i : LeftMoves y
⊢ P (↑toLeftMovesAdd (Sum.inr i))
[PROOFSTEP]
exact hr i
[GOAL]
x y : PGame
k : RightMoves (x + y)
P : RightMoves (x + y) → Prop
hl : ∀ (j : RightMoves x), P (↑toRightMovesAdd (Sum.inl j))
hr : ∀ (j : RightMoves y), P (↑toRightMovesAdd (Sum.inr j))
⊢ P k
[PROOFSTEP]
rw [← toRightMovesAdd.apply_symm_apply k]
[GOAL]
x y : PGame
k : RightMoves (x + y)
P : RightMoves (x + y) → Prop
hl : ∀ (j : RightMoves x), P (↑toRightMovesAdd (Sum.inl j))
hr : ∀ (j : RightMoves y), P (↑toRightMovesAdd (Sum.inr j))
⊢ P (↑toRightMovesAdd (↑toRightMovesAdd.symm k))
[PROOFSTEP]
cases' toRightMovesAdd.symm k with i i
[GOAL]
case inl
x y : PGame
k : RightMoves (x + y)
P : RightMoves (x + y) → Prop
hl : ∀ (j : RightMoves x), P (↑toRightMovesAdd (Sum.inl j))
hr : ∀ (j : RightMoves y), P (↑toRightMovesAdd (Sum.inr j))
i : RightMoves x
⊢ P (↑toRightMovesAdd (Sum.inl i))
[PROOFSTEP]
exact hl i
[GOAL]
case inr
x y : PGame
k : RightMoves (x + y)
P : RightMoves (x + y) → Prop
hl : ∀ (j : RightMoves x), P (↑toRightMovesAdd (Sum.inl j))
hr : ∀ (j : RightMoves y), P (↑toRightMovesAdd (Sum.inr j))
i : RightMoves y
⊢ P (↑toRightMovesAdd (Sum.inr i))
[PROOFSTEP]
exact hr i
[GOAL]
n : ℕ
⊢ IsEmpty (RightMoves ↑(n + 1))
[PROOFSTEP]
haveI := isEmpty_nat_rightMoves n
[GOAL]
n : ℕ
this : IsEmpty (RightMoves ↑n)
⊢ IsEmpty (RightMoves ↑(n + 1))
[PROOFSTEP]
rw [PGame.nat_succ, rightMoves_add]
[GOAL]
n : ℕ
this : IsEmpty (RightMoves ↑n)
⊢ IsEmpty (RightMoves ↑n ⊕ RightMoves 1)
[PROOFSTEP]
infer_instance
[GOAL]
wl wr : Type u
wL : wl → PGame
wR : wr → PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
L₁ : LeftMoves (PGame.mk wl wr wL wR) ≃ LeftMoves (PGame.mk xl xr xL xR)
R₁ : RightMoves (PGame.mk wl wr wL wR) ≃ RightMoves (PGame.mk xl xr xL xR)
hL₁ :
  (i : LeftMoves (PGame.mk wl wr wL wR)) →
    PGame.moveLeft (PGame.mk wl wr wL wR) i ≡r PGame.moveLeft (PGame.mk xl xr xL xR) (↑L₁ i)
hR₁ :
  (j : RightMoves (PGame.mk wl wr wL wR)) →
    PGame.moveRight (PGame.mk wl wr wL wR) j ≡r PGame.moveRight (PGame.mk xl xr xL xR) (↑R₁ j)
L₂ : LeftMoves (PGame.mk yl yr yL yR) ≃ LeftMoves (PGame.mk zl zr zL zR)
R₂ : RightMoves (PGame.mk yl yr yL yR) ≃ RightMoves (PGame.mk zl zr zL zR)
hL₂ :
  (i : LeftMoves (PGame.mk yl yr yL yR)) →
    PGame.moveLeft (PGame.mk yl yr yL yR) i ≡r PGame.moveLeft (PGame.mk zl zr zL zR) (↑L₂ i)
hR₂ :
  (j : RightMoves (PGame.mk yl yr yL yR)) →
    PGame.moveRight (PGame.mk yl yr yL yR) j ≡r PGame.moveRight (PGame.mk zl zr zL zR) (↑R₂ j)
⊢ PGame.mk wl wr wL wR + PGame.mk yl yr yL yR ≡r PGame.mk xl xr xL xR + PGame.mk zl zr zL zR
[PROOFSTEP]
let Hwx : ⟨wl, wr, wL, wR⟩ ≡r ⟨xl, xr, xL, xR⟩ := ⟨L₁, R₁, hL₁, hR₁⟩
[GOAL]
wl wr : Type u
wL : wl → PGame
wR : wr → PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
L₁ : LeftMoves (PGame.mk wl wr wL wR) ≃ LeftMoves (PGame.mk xl xr xL xR)
R₁ : RightMoves (PGame.mk wl wr wL wR) ≃ RightMoves (PGame.mk xl xr xL xR)
hL₁ :
  (i : LeftMoves (PGame.mk wl wr wL wR)) →
    PGame.moveLeft (PGame.mk wl wr wL wR) i ≡r PGame.moveLeft (PGame.mk xl xr xL xR) (↑L₁ i)
hR₁ :
  (j : RightMoves (PGame.mk wl wr wL wR)) →
    PGame.moveRight (PGame.mk wl wr wL wR) j ≡r PGame.moveRight (PGame.mk xl xr xL xR) (↑R₁ j)
L₂ : LeftMoves (PGame.mk yl yr yL yR) ≃ LeftMoves (PGame.mk zl zr zL zR)
R₂ : RightMoves (PGame.mk yl yr yL yR) ≃ RightMoves (PGame.mk zl zr zL zR)
hL₂ :
  (i : LeftMoves (PGame.mk yl yr yL yR)) →
    PGame.moveLeft (PGame.mk yl yr yL yR) i ≡r PGame.moveLeft (PGame.mk zl zr zL zR) (↑L₂ i)
hR₂ :
  (j : RightMoves (PGame.mk yl yr yL yR)) →
    PGame.moveRight (PGame.mk yl yr yL yR) j ≡r PGame.moveRight (PGame.mk zl zr zL zR) (↑R₂ j)
Hwx : PGame.mk wl wr wL wR ≡r PGame.mk xl xr xL xR := mk L₁ R₁ hL₁ hR₁
⊢ PGame.mk wl wr wL wR + PGame.mk yl yr yL yR ≡r PGame.mk xl xr xL xR + PGame.mk zl zr zL zR
[PROOFSTEP]
let Hyz : ⟨yl, yr, yL, yR⟩ ≡r ⟨zl, zr, zL, zR⟩ := ⟨L₂, R₂, hL₂, hR₂⟩
[GOAL]
wl wr : Type u
wL : wl → PGame
wR : wr → PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
L₁ : LeftMoves (PGame.mk wl wr wL wR) ≃ LeftMoves (PGame.mk xl xr xL xR)
R₁ : RightMoves (PGame.mk wl wr wL wR) ≃ RightMoves (PGame.mk xl xr xL xR)
hL₁ :
  (i : LeftMoves (PGame.mk wl wr wL wR)) →
    PGame.moveLeft (PGame.mk wl wr wL wR) i ≡r PGame.moveLeft (PGame.mk xl xr xL xR) (↑L₁ i)
hR₁ :
  (j : RightMoves (PGame.mk wl wr wL wR)) →
    PGame.moveRight (PGame.mk wl wr wL wR) j ≡r PGame.moveRight (PGame.mk xl xr xL xR) (↑R₁ j)
L₂ : LeftMoves (PGame.mk yl yr yL yR) ≃ LeftMoves (PGame.mk zl zr zL zR)
R₂ : RightMoves (PGame.mk yl yr yL yR) ≃ RightMoves (PGame.mk zl zr zL zR)
hL₂ :
  (i : LeftMoves (PGame.mk yl yr yL yR)) →
    PGame.moveLeft (PGame.mk yl yr yL yR) i ≡r PGame.moveLeft (PGame.mk zl zr zL zR) (↑L₂ i)
hR₂ :
  (j : RightMoves (PGame.mk yl yr yL yR)) →
    PGame.moveRight (PGame.mk yl yr yL yR) j ≡r PGame.moveRight (PGame.mk zl zr zL zR) (↑R₂ j)
Hwx : PGame.mk wl wr wL wR ≡r PGame.mk xl xr xL xR := mk L₁ R₁ hL₁ hR₁
Hyz : PGame.mk yl yr yL yR ≡r PGame.mk zl zr zL zR := mk L₂ R₂ hL₂ hR₂
⊢ PGame.mk wl wr wL wR + PGame.mk yl yr yL yR ≡r PGame.mk xl xr xL xR + PGame.mk zl zr zL zR
[PROOFSTEP]
refine' ⟨Equiv.sumCongr L₁ L₂, Equiv.sumCongr R₁ R₂, _, _⟩
[GOAL]
case refine'_1
wl wr : Type u
wL : wl → PGame
wR : wr → PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
L₁ : LeftMoves (PGame.mk wl wr wL wR) ≃ LeftMoves (PGame.mk xl xr xL xR)
R₁ : RightMoves (PGame.mk wl wr wL wR) ≃ RightMoves (PGame.mk xl xr xL xR)
hL₁ :
  (i : LeftMoves (PGame.mk wl wr wL wR)) →
    PGame.moveLeft (PGame.mk wl wr wL wR) i ≡r PGame.moveLeft (PGame.mk xl xr xL xR) (↑L₁ i)
hR₁ :
  (j : RightMoves (PGame.mk wl wr wL wR)) →
    PGame.moveRight (PGame.mk wl wr wL wR) j ≡r PGame.moveRight (PGame.mk xl xr xL xR) (↑R₁ j)
L₂ : LeftMoves (PGame.mk yl yr yL yR) ≃ LeftMoves (PGame.mk zl zr zL zR)
R₂ : RightMoves (PGame.mk yl yr yL yR) ≃ RightMoves (PGame.mk zl zr zL zR)
hL₂ :
  (i : LeftMoves (PGame.mk yl yr yL yR)) →
    PGame.moveLeft (PGame.mk yl yr yL yR) i ≡r PGame.moveLeft (PGame.mk zl zr zL zR) (↑L₂ i)
hR₂ :
  (j : RightMoves (PGame.mk yl yr yL yR)) →
    PGame.moveRight (PGame.mk yl yr yL yR) j ≡r PGame.moveRight (PGame.mk zl zr zL zR) (↑R₂ j)
Hwx : PGame.mk wl wr wL wR ≡r PGame.mk xl xr xL xR := mk L₁ R₁ hL₁ hR₁
Hyz : PGame.mk yl yr yL yR ≡r PGame.mk zl zr zL zR := mk L₂ R₂ hL₂ hR₂
⊢ (i : LeftMoves (PGame.mk wl wr wL wR + PGame.mk yl yr yL yR)) →
    PGame.moveLeft (PGame.mk wl wr wL wR + PGame.mk yl yr yL yR) i ≡r
      PGame.moveLeft (PGame.mk xl xr xL xR + PGame.mk zl zr zL zR) (↑(Equiv.sumCongr L₁ L₂) i)
[PROOFSTEP]
rintro (i | j)
[GOAL]
case refine'_2
wl wr : Type u
wL : wl → PGame
wR : wr → PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
L₁ : LeftMoves (PGame.mk wl wr wL wR) ≃ LeftMoves (PGame.mk xl xr xL xR)
R₁ : RightMoves (PGame.mk wl wr wL wR) ≃ RightMoves (PGame.mk xl xr xL xR)
hL₁ :
  (i : LeftMoves (PGame.mk wl wr wL wR)) →
    PGame.moveLeft (PGame.mk wl wr wL wR) i ≡r PGame.moveLeft (PGame.mk xl xr xL xR) (↑L₁ i)
hR₁ :
  (j : RightMoves (PGame.mk wl wr wL wR)) →
    PGame.moveRight (PGame.mk wl wr wL wR) j ≡r PGame.moveRight (PGame.mk xl xr xL xR) (↑R₁ j)
L₂ : LeftMoves (PGame.mk yl yr yL yR) ≃ LeftMoves (PGame.mk zl zr zL zR)
R₂ : RightMoves (PGame.mk yl yr yL yR) ≃ RightMoves (PGame.mk zl zr zL zR)
hL₂ :
  (i : LeftMoves (PGame.mk yl yr yL yR)) →
    PGame.moveLeft (PGame.mk yl yr yL yR) i ≡r PGame.moveLeft (PGame.mk zl zr zL zR) (↑L₂ i)
hR₂ :
  (j : RightMoves (PGame.mk yl yr yL yR)) →
    PGame.moveRight (PGame.mk yl yr yL yR) j ≡r PGame.moveRight (PGame.mk zl zr zL zR) (↑R₂ j)
Hwx : PGame.mk wl wr wL wR ≡r PGame.mk xl xr xL xR := mk L₁ R₁ hL₁ hR₁
Hyz : PGame.mk yl yr yL yR ≡r PGame.mk zl zr zL zR := mk L₂ R₂ hL₂ hR₂
⊢ (j : RightMoves (PGame.mk wl wr wL wR + PGame.mk yl yr yL yR)) →
    PGame.moveRight (PGame.mk wl wr wL wR + PGame.mk yl yr yL yR) j ≡r
      PGame.moveRight (PGame.mk xl xr xL xR + PGame.mk zl zr zL zR) (↑(Equiv.sumCongr R₁ R₂) j)
[PROOFSTEP]
rintro (i | j)
[GOAL]
case refine'_1.inl
wl wr : Type u
wL : wl → PGame
wR : wr → PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
L₁ : LeftMoves (PGame.mk wl wr wL wR) ≃ LeftMoves (PGame.mk xl xr xL xR)
R₁ : RightMoves (PGame.mk wl wr wL wR) ≃ RightMoves (PGame.mk xl xr xL xR)
hL₁ :
  (i : LeftMoves (PGame.mk wl wr wL wR)) →
    PGame.moveLeft (PGame.mk wl wr wL wR) i ≡r PGame.moveLeft (PGame.mk xl xr xL xR) (↑L₁ i)
hR₁ :
  (j : RightMoves (PGame.mk wl wr wL wR)) →
    PGame.moveRight (PGame.mk wl wr wL wR) j ≡r PGame.moveRight (PGame.mk xl xr xL xR) (↑R₁ j)
L₂ : LeftMoves (PGame.mk yl yr yL yR) ≃ LeftMoves (PGame.mk zl zr zL zR)
R₂ : RightMoves (PGame.mk yl yr yL yR) ≃ RightMoves (PGame.mk zl zr zL zR)
hL₂ :
  (i : LeftMoves (PGame.mk yl yr yL yR)) →
    PGame.moveLeft (PGame.mk yl yr yL yR) i ≡r PGame.moveLeft (PGame.mk zl zr zL zR) (↑L₂ i)
hR₂ :
  (j : RightMoves (PGame.mk yl yr yL yR)) →
    PGame.moveRight (PGame.mk yl yr yL yR) j ≡r PGame.moveRight (PGame.mk zl zr zL zR) (↑R₂ j)
Hwx : PGame.mk wl wr wL wR ≡r PGame.mk xl xr xL xR := mk L₁ R₁ hL₁ hR₁
Hyz : PGame.mk yl yr yL yR ≡r PGame.mk zl zr zL zR := mk L₂ R₂ hL₂ hR₂
i : wl
⊢ PGame.moveLeft (PGame.mk wl wr wL wR + PGame.mk yl yr yL yR) (Sum.inl i) ≡r
    PGame.moveLeft (PGame.mk xl xr xL xR + PGame.mk zl zr zL zR) (↑(Equiv.sumCongr L₁ L₂) (Sum.inl i))
[PROOFSTEP]
exact (hL₁ i).addCongr Hyz
[GOAL]
case refine'_1.inr
wl wr : Type u
wL : wl → PGame
wR : wr → PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
L₁ : LeftMoves (PGame.mk wl wr wL wR) ≃ LeftMoves (PGame.mk xl xr xL xR)
R₁ : RightMoves (PGame.mk wl wr wL wR) ≃ RightMoves (PGame.mk xl xr xL xR)
hL₁ :
  (i : LeftMoves (PGame.mk wl wr wL wR)) →
    PGame.moveLeft (PGame.mk wl wr wL wR) i ≡r PGame.moveLeft (PGame.mk xl xr xL xR) (↑L₁ i)
hR₁ :
  (j : RightMoves (PGame.mk wl wr wL wR)) →
    PGame.moveRight (PGame.mk wl wr wL wR) j ≡r PGame.moveRight (PGame.mk xl xr xL xR) (↑R₁ j)
L₂ : LeftMoves (PGame.mk yl yr yL yR) ≃ LeftMoves (PGame.mk zl zr zL zR)
R₂ : RightMoves (PGame.mk yl yr yL yR) ≃ RightMoves (PGame.mk zl zr zL zR)
hL₂ :
  (i : LeftMoves (PGame.mk yl yr yL yR)) →
    PGame.moveLeft (PGame.mk yl yr yL yR) i ≡r PGame.moveLeft (PGame.mk zl zr zL zR) (↑L₂ i)
hR₂ :
  (j : RightMoves (PGame.mk yl yr yL yR)) →
    PGame.moveRight (PGame.mk yl yr yL yR) j ≡r PGame.moveRight (PGame.mk zl zr zL zR) (↑R₂ j)
Hwx : PGame.mk wl wr wL wR ≡r PGame.mk xl xr xL xR := mk L₁ R₁ hL₁ hR₁
Hyz : PGame.mk yl yr yL yR ≡r PGame.mk zl zr zL zR := mk L₂ R₂ hL₂ hR₂
j : yl
⊢ PGame.moveLeft (PGame.mk wl wr wL wR + PGame.mk yl yr yL yR) (Sum.inr j) ≡r
    PGame.moveLeft (PGame.mk xl xr xL xR + PGame.mk zl zr zL zR) (↑(Equiv.sumCongr L₁ L₂) (Sum.inr j))
[PROOFSTEP]
exact Hwx.addCongr (hL₂ j)
[GOAL]
case refine'_2.inl
wl wr : Type u
wL : wl → PGame
wR : wr → PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
L₁ : LeftMoves (PGame.mk wl wr wL wR) ≃ LeftMoves (PGame.mk xl xr xL xR)
R₁ : RightMoves (PGame.mk wl wr wL wR) ≃ RightMoves (PGame.mk xl xr xL xR)
hL₁ :
  (i : LeftMoves (PGame.mk wl wr wL wR)) →
    PGame.moveLeft (PGame.mk wl wr wL wR) i ≡r PGame.moveLeft (PGame.mk xl xr xL xR) (↑L₁ i)
hR₁ :
  (j : RightMoves (PGame.mk wl wr wL wR)) →
    PGame.moveRight (PGame.mk wl wr wL wR) j ≡r PGame.moveRight (PGame.mk xl xr xL xR) (↑R₁ j)
L₂ : LeftMoves (PGame.mk yl yr yL yR) ≃ LeftMoves (PGame.mk zl zr zL zR)
R₂ : RightMoves (PGame.mk yl yr yL yR) ≃ RightMoves (PGame.mk zl zr zL zR)
hL₂ :
  (i : LeftMoves (PGame.mk yl yr yL yR)) →
    PGame.moveLeft (PGame.mk yl yr yL yR) i ≡r PGame.moveLeft (PGame.mk zl zr zL zR) (↑L₂ i)
hR₂ :
  (j : RightMoves (PGame.mk yl yr yL yR)) →
    PGame.moveRight (PGame.mk yl yr yL yR) j ≡r PGame.moveRight (PGame.mk zl zr zL zR) (↑R₂ j)
Hwx : PGame.mk wl wr wL wR ≡r PGame.mk xl xr xL xR := mk L₁ R₁ hL₁ hR₁
Hyz : PGame.mk yl yr yL yR ≡r PGame.mk zl zr zL zR := mk L₂ R₂ hL₂ hR₂
i : wr
⊢ PGame.moveRight (PGame.mk wl wr wL wR + PGame.mk yl yr yL yR) (Sum.inl i) ≡r
    PGame.moveRight (PGame.mk xl xr xL xR + PGame.mk zl zr zL zR) (↑(Equiv.sumCongr R₁ R₂) (Sum.inl i))
[PROOFSTEP]
exact (hR₁ i).addCongr Hyz
[GOAL]
case refine'_2.inr
wl wr : Type u
wL : wl → PGame
wR : wr → PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
L₁ : LeftMoves (PGame.mk wl wr wL wR) ≃ LeftMoves (PGame.mk xl xr xL xR)
R₁ : RightMoves (PGame.mk wl wr wL wR) ≃ RightMoves (PGame.mk xl xr xL xR)
hL₁ :
  (i : LeftMoves (PGame.mk wl wr wL wR)) →
    PGame.moveLeft (PGame.mk wl wr wL wR) i ≡r PGame.moveLeft (PGame.mk xl xr xL xR) (↑L₁ i)
hR₁ :
  (j : RightMoves (PGame.mk wl wr wL wR)) →
    PGame.moveRight (PGame.mk wl wr wL wR) j ≡r PGame.moveRight (PGame.mk xl xr xL xR) (↑R₁ j)
L₂ : LeftMoves (PGame.mk yl yr yL yR) ≃ LeftMoves (PGame.mk zl zr zL zR)
R₂ : RightMoves (PGame.mk yl yr yL yR) ≃ RightMoves (PGame.mk zl zr zL zR)
hL₂ :
  (i : LeftMoves (PGame.mk yl yr yL yR)) →
    PGame.moveLeft (PGame.mk yl yr yL yR) i ≡r PGame.moveLeft (PGame.mk zl zr zL zR) (↑L₂ i)
hR₂ :
  (j : RightMoves (PGame.mk yl yr yL yR)) →
    PGame.moveRight (PGame.mk yl yr yL yR) j ≡r PGame.moveRight (PGame.mk zl zr zL zR) (↑R₂ j)
Hwx : PGame.mk wl wr wL wR ≡r PGame.mk xl xr xL xR := mk L₁ R₁ hL₁ hR₁
Hyz : PGame.mk yl yr yL yR ≡r PGame.mk zl zr zL zR := mk L₂ R₂ hL₂ hR₂
j : yr
⊢ PGame.moveRight (PGame.mk wl wr wL wR + PGame.mk yl yr yL yR) (Sum.inr j) ≡r
    PGame.moveRight (PGame.mk xl xr xL xR + PGame.mk zl zr zL zR) (↑(Equiv.sumCongr R₁ R₂) (Sum.inr j))
[PROOFSTEP]
exact Hwx.addCongr (hR₂ j)
[GOAL]
x : PGame
⊢ x + -0 = x + 0
[PROOFSTEP]
rw [neg_zero]
[GOAL]
xl xr : Type ?u.151060
xL : xl → PGame
xR : xr → PGame
yl yr : Type ?u.151060
yL : yl → PGame
yR : yr → PGame
⊢ -(mk xl xr xL xR + mk yl yr yL yR) ≡r -mk xl xr xL xR + -mk yl yr yL yR
[PROOFSTEP]
refine' ⟨Equiv.refl _, Equiv.refl _, _, _⟩
[GOAL]
case refine'_1
xl xr : Type ?u.151060
xL : xl → PGame
xR : xr → PGame
yl yr : Type ?u.151060
yL : yl → PGame
yR : yr → PGame
⊢ (i : LeftMoves (-(mk xl xr xL xR + mk yl yr yL yR))) →
    moveLeft (-(mk xl xr xL xR + mk yl yr yL yR)) i ≡r
      moveLeft (-mk xl xr xL xR + -mk yl yr yL yR) (↑(Equiv.refl (LeftMoves (-(mk xl xr xL xR + mk yl yr yL yR)))) i)
case refine'_2
xl xr : Type ?u.151060
xL : xl → PGame
xR : xr → PGame
yl yr : Type ?u.151060
yL : yl → PGame
yR : yr → PGame
⊢ (j : RightMoves (-(mk xl xr xL xR + mk yl yr yL yR))) →
    moveRight (-(mk xl xr xL xR + mk yl yr yL yR)) j ≡r
      moveRight (-mk xl xr xL xR + -mk yl yr yL yR) (↑(Equiv.refl (RightMoves (-(mk xl xr xL xR + mk yl yr yL yR)))) j)
[PROOFSTEP]
all_goals exact fun j => Sum.casesOn j (fun j => negAddRelabelling _ _) fun j => negAddRelabelling ⟨xl, xr, xL, xR⟩ _
[GOAL]
case refine'_1
xl xr : Type ?u.151060
xL : xl → PGame
xR : xr → PGame
yl yr : Type ?u.151060
yL : yl → PGame
yR : yr → PGame
⊢ (i : LeftMoves (-(mk xl xr xL xR + mk yl yr yL yR))) →
    moveLeft (-(mk xl xr xL xR + mk yl yr yL yR)) i ≡r
      moveLeft (-mk xl xr xL xR + -mk yl yr yL yR) (↑(Equiv.refl (LeftMoves (-(mk xl xr xL xR + mk yl yr yL yR)))) i)
[PROOFSTEP]
exact fun j => Sum.casesOn j (fun j => negAddRelabelling _ _) fun j => negAddRelabelling ⟨xl, xr, xL, xR⟩ _
[GOAL]
case refine'_2
xl xr : Type ?u.151807
xL : xl → PGame
xR : xr → PGame
yl yr : Type ?u.151807
yL : yl → PGame
yR : yr → PGame
⊢ (j : RightMoves (-(mk xl xr xL xR + mk yl yr yL yR))) →
    moveRight (-(mk xl xr xL xR + mk yl yr yL yR)) j ≡r
      moveRight (-mk xl xr xL xR + -mk yl yr yL yR) (↑(Equiv.refl (RightMoves (-(mk xl xr xL xR + mk yl yr yL yR)))) j)
[PROOFSTEP]
exact fun j => Sum.casesOn j (fun j => negAddRelabelling _ _) fun j => negAddRelabelling ⟨xl, xr, xL, xR⟩ _
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ mk xl xr xL xR + mk yl yr yL yR ≡r mk yl yr yL yR + mk xl xr xL xR
[PROOFSTEP]
refine' ⟨Equiv.sumComm _ _, Equiv.sumComm _ _, _, _⟩
[GOAL]
case refine'_1
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (i : LeftMoves (mk xl xr xL xR + mk yl yr yL yR)) →
    moveLeft (mk xl xr xL xR + mk yl yr yL yR) i ≡r
      moveLeft (mk yl yr yL yR + mk xl xr xL xR) (↑(Equiv.sumComm xl yl) i)
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case refine'_2
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (j : RightMoves (mk xl xr xL xR + mk yl yr yL yR)) →
    moveRight (mk xl xr xL xR + mk yl yr yL yR) j ≡r
      moveRight (mk yl yr yL yR + mk xl xr xL xR) (↑(Equiv.sumComm xr yr) j)
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case refine'_1.inl
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
val✝ : xl
⊢ moveLeft (mk xl xr xL xR + mk yl yr yL yR) (Sum.inl val✝) ≡r
    moveLeft (mk yl yr yL yR + mk xl xr xL xR) (↑(Equiv.sumComm xl yl) (Sum.inl val✝))
[PROOFSTEP]
dsimp [leftMoves_add, rightMoves_add]
[GOAL]
case refine'_1.inl
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
val✝ : xl
⊢ xL val✝ + mk yl yr yL yR ≡r moveLeft (mk yl yr yL yR + mk xl xr xL xR) (↑(Equiv.sumComm xl yl) (Sum.inl val✝))
[PROOFSTEP]
apply addCommRelabelling
[GOAL]
case refine'_1.inr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
val✝ : yl
⊢ moveLeft (mk xl xr xL xR + mk yl yr yL yR) (Sum.inr val✝) ≡r
    moveLeft (mk yl yr yL yR + mk xl xr xL xR) (↑(Equiv.sumComm xl yl) (Sum.inr val✝))
[PROOFSTEP]
dsimp [leftMoves_add, rightMoves_add]
[GOAL]
case refine'_1.inr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
val✝ : yl
⊢ mk xl xr xL xR + yL val✝ ≡r moveLeft (mk yl yr yL yR + mk xl xr xL xR) (↑(Equiv.sumComm xl yl) (Sum.inr val✝))
[PROOFSTEP]
apply addCommRelabelling
[GOAL]
case refine'_2.inl
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
val✝ : xr
⊢ moveRight (mk xl xr xL xR + mk yl yr yL yR) (Sum.inl val✝) ≡r
    moveRight (mk yl yr yL yR + mk xl xr xL xR) (↑(Equiv.sumComm xr yr) (Sum.inl val✝))
[PROOFSTEP]
dsimp [leftMoves_add, rightMoves_add]
[GOAL]
case refine'_2.inl
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
val✝ : xr
⊢ xR val✝ + mk yl yr yL yR ≡r moveRight (mk yl yr yL yR + mk xl xr xL xR) (↑(Equiv.sumComm xr yr) (Sum.inl val✝))
[PROOFSTEP]
apply addCommRelabelling
[GOAL]
case refine'_2.inr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
val✝ : yr
⊢ moveRight (mk xl xr xL xR + mk yl yr yL yR) (Sum.inr val✝) ≡r
    moveRight (mk yl yr yL yR + mk xl xr xL xR) (↑(Equiv.sumComm xr yr) (Sum.inr val✝))
[PROOFSTEP]
dsimp [leftMoves_add, rightMoves_add]
[GOAL]
case refine'_2.inr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
val✝ : yr
⊢ mk xl xr xL xR + yR val✝ ≡r moveRight (mk yl yr yL yR + mk xl xr xL xR) (↑(Equiv.sumComm xr yr) (Sum.inr val✝))
[PROOFSTEP]
apply addCommRelabelling
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
⊢ mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR ≡r mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)
[PROOFSTEP]
refine' ⟨Equiv.sumAssoc _ _ _, Equiv.sumAssoc _ _ _, _, _⟩
[GOAL]
case refine'_1
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
⊢ (i : LeftMoves (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR)) →
    moveLeft (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR) i ≡r
      moveLeft (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)) (↑(Equiv.sumAssoc xl yl zl) i)
[PROOFSTEP]
rintro (⟨i | i⟩ | i)
[GOAL]
case refine'_1.inl.inl
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
i : xl
⊢ moveLeft (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR) (Sum.inl (Sum.inl i)) ≡r
    moveLeft (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)) (↑(Equiv.sumAssoc xl yl zl) (Sum.inl (Sum.inl i)))
[PROOFSTEP]
apply addAssocRelabelling
[GOAL]
case refine'_1.inl.inr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
i : yl
⊢ moveLeft (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR) (Sum.inl (Sum.inr i)) ≡r
    moveLeft (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)) (↑(Equiv.sumAssoc xl yl zl) (Sum.inl (Sum.inr i)))
[PROOFSTEP]
apply addAssocRelabelling ⟨xl, xr, xL, xR⟩ (yL i)
[GOAL]
case refine'_1.inr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
i : zl
⊢ moveLeft (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR) (Sum.inr i) ≡r
    moveLeft (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)) (↑(Equiv.sumAssoc xl yl zl) (Sum.inr i))
[PROOFSTEP]
apply addAssocRelabelling ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ (zL i)
[GOAL]
case refine'_2
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
⊢ (j : RightMoves (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR)) →
    moveRight (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR) j ≡r
      moveRight (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)) (↑(Equiv.sumAssoc xr yr zr) j)
[PROOFSTEP]
rintro (⟨i | i⟩ | i)
[GOAL]
case refine'_2.inl.inl
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
i : xr
⊢ moveRight (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR) (Sum.inl (Sum.inl i)) ≡r
    moveRight (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)) (↑(Equiv.sumAssoc xr yr zr) (Sum.inl (Sum.inl i)))
[PROOFSTEP]
apply addAssocRelabelling
[GOAL]
case refine'_2.inl.inr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
i : yr
⊢ moveRight (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR) (Sum.inl (Sum.inr i)) ≡r
    moveRight (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)) (↑(Equiv.sumAssoc xr yr zr) (Sum.inl (Sum.inr i)))
[PROOFSTEP]
apply addAssocRelabelling ⟨xl, xr, xL, xR⟩ (yR i)
[GOAL]
case refine'_2.inr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
zl zr : Type u
zL : zl → PGame
zR : zr → PGame
i : zr
⊢ moveRight (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR) (Sum.inr i) ≡r
    moveRight (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)) (↑(Equiv.sumAssoc xr yr zr) (Sum.inr i))
[PROOFSTEP]
apply addAssocRelabelling ⟨xl, xr, xL, xR⟩ ⟨yl, yr, yL, yR⟩ (zR i)
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : LeftMoves (-mk xl xr xL xR + mk xl xr xL xR)
⊢ ∃ j, moveRight (moveLeft (-mk xl xr xL xR + mk xl xr xL xR) i) j ≤ 0
[PROOFSTEP]
cases' i with i i
[GOAL]
case inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ ∃ j, moveRight (moveLeft (-mk xl xr xL xR + mk xl xr xL xR) (Sum.inl i)) j ≤ 0
[PROOFSTEP]
refine' ⟨@toRightMovesAdd _ ⟨_, _, _, _⟩ (Sum.inr i), _⟩
[GOAL]
case inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ moveRight (moveLeft (-mk xl xr xL xR + mk xl xr xL xR) (Sum.inl i)) (↑toRightMovesAdd (Sum.inr i)) ≤ 0
[PROOFSTEP]
convert @add_left_neg_le_zero (xR i)
[GOAL]
case h.e'_3
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ moveRight (moveLeft (-mk xl xr xL xR + mk xl xr xL xR) (Sum.inl i)) (↑toRightMovesAdd (Sum.inr i)) = -xR i + xR i
[PROOFSTEP]
apply add_moveRight_inr
[GOAL]
case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ ∃ j, moveRight (moveLeft (-mk xl xr xL xR + mk xl xr xL xR) (Sum.inr i)) j ≤ 0
[PROOFSTEP]
dsimp
[GOAL]
case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ ∃ j, moveRight ((mk xr xl (fun j => -xR j) fun i => -xL i) + xL i) j ≤ 0
[PROOFSTEP]
refine' ⟨@toRightMovesAdd ⟨_, _, _, _⟩ _ (Sum.inl i), _⟩
[GOAL]
case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ moveRight ((mk xr xl (fun j => -xR j) fun i => -xL i) + xL i) (↑toRightMovesAdd (Sum.inl i)) ≤ 0
[PROOFSTEP]
convert @add_left_neg_le_zero (xL i)
[GOAL]
case h.e'_3
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ moveRight ((mk xr xl (fun j => -xR j) fun i => -xL i) + xL i) (↑toRightMovesAdd (Sum.inl i)) = -xL i + xL i
[PROOFSTEP]
apply add_moveRight_inl
[GOAL]
x : PGame
⊢ 0 ≤ -x + x
[PROOFSTEP]
rw [← neg_le_neg_iff, neg_zero]
[GOAL]
x : PGame
⊢ -(-x + x) ≤ 0
[PROOFSTEP]
exact neg_add_le.trans (add_left_neg_le_zero _)
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
⊢ mk xl xr xL xR + mk zl zr zL zR ≤ mk yl yr yL yR + mk zl zr zL zR
[PROOFSTEP]
refine' le_def.2 ⟨fun i => _, fun i => _⟩
[GOAL]
case refine'_1
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
i : LeftMoves (mk xl xr xL xR + mk zl zr zL zR)
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) i ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) i) j ≤ mk yl yr yL yR + mk zl zr zL zR
[PROOFSTEP]
cases' i with i i
[GOAL]
case refine'_2
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
i : RightMoves (mk yl yr yL yR + mk zl zr zL zR)
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) i) i_1) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) i
[PROOFSTEP]
cases' i with i i
[GOAL]
case refine'_1.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
i : xl
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
[PROOFSTEP]
rw [le_def] at h
[GOAL]
case refine'_1.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i : xl
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
[PROOFSTEP]
cases' h with h_left h_right
[GOAL]
case refine'_1.inl.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
[PROOFSTEP]
rcases h_left i with (⟨i', ih⟩ | ⟨j, jh⟩)
[GOAL]
case refine'_1.inl.intro.inl.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i' : LeftMoves (mk yl yr yL yR)
ih : moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i'
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
[PROOFSTEP]
exact Or.inl ⟨toLeftMovesAdd (Sum.inl i'), add_le_add_right' ih⟩
[GOAL]
case refine'_1.inl.intro.inr.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
j : RightMoves (moveLeft (mk xl xr xL xR) i)
jh : moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
[PROOFSTEP]
refine' Or.inr ⟨toRightMovesAdd (Sum.inl j), _⟩
[GOAL]
case refine'_1.inl.intro.inr.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
j : RightMoves (moveLeft (mk xl xr xL xR) i)
jh : moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
⊢ moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) (↑toRightMovesAdd (Sum.inl j)) ≤
    mk yl yr yL yR + mk zl zr zL zR
[PROOFSTEP]
convert add_le_add_right' jh
[GOAL]
case h.e'_3
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
j : RightMoves (moveLeft (mk xl xr xL xR) i)
jh : moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
⊢ moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) (↑toRightMovesAdd (Sum.inl j)) =
    moveRight (moveLeft (mk xl xr xL xR) i) j + mk zl zr zL zR
[PROOFSTEP]
apply add_moveRight_inl
[GOAL]
case refine'_1.inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
i : zl
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inr i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inr i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
[PROOFSTEP]
exact Or.inl ⟨@toLeftMovesAdd _ ⟨_, _, _, _⟩ (Sum.inr i), add_le_add_right' h⟩
[GOAL]
case refine'_2.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
i : yr
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)) i_1) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)
[PROOFSTEP]
rw [le_def] at h
[GOAL]
case refine'_2.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i : yr
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)) i_1) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)
[PROOFSTEP]
rcases h.right i with (⟨i, ih⟩ | ⟨j', jh⟩)
[GOAL]
case refine'_2.inl.inl.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i✝ : yr
i : LeftMoves (moveRight (mk yl yr yL yR) i✝)
ih : mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) i✝) i
⊢ (∃ i, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i✝)) i) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i✝)
[PROOFSTEP]
refine' Or.inl ⟨toLeftMovesAdd (Sum.inl i), _⟩
[GOAL]
case refine'_2.inl.inl.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i✝ : yr
i : LeftMoves (moveRight (mk yl yr yL yR) i✝)
ih : mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) i✝) i
⊢ mk xl xr xL xR + mk zl zr zL zR ≤
    moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i✝)) (↑toLeftMovesAdd (Sum.inl i))
[PROOFSTEP]
convert add_le_add_right' ih
[GOAL]
case h.e'_4
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i✝ : yr
i : LeftMoves (moveRight (mk yl yr yL yR) i✝)
ih : mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) i✝) i
⊢ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i✝)) (↑toLeftMovesAdd (Sum.inl i)) =
    moveLeft (moveRight (mk yl yr yL yR) i✝) i + mk zl zr zL zR
[PROOFSTEP]
apply add_moveLeft_inl
[GOAL]
case refine'_2.inl.inr.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i : yr
j' : RightMoves (mk xl xr xL xR)
jh : moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) i
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)) i_1) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)
[PROOFSTEP]
exact Or.inr ⟨toRightMovesAdd (Sum.inl j'), add_le_add_right' jh⟩
[GOAL]
case refine'_2.inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
i : zr
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inr i)) i_1) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inr i)
[PROOFSTEP]
exact Or.inr ⟨@toRightMovesAdd _ ⟨_, _, _, _⟩ (Sum.inr i), add_le_add_right' h⟩
[GOAL]
y z : PGame
h : y ⧏ z
x : PGame
this : z + x ≤ y + x → z ≤ y
⊢ y + x ⧏ z + x
[PROOFSTEP]
rw [← PGame.not_le] at h ⊢
[GOAL]
y z : PGame
h : ¬z ≤ y
x : PGame
this : z + x ≤ y + x → z ≤ y
⊢ ¬z + x ≤ y + x
[PROOFSTEP]
exact mt this h
[GOAL]
y z : PGame
h : y ⧏ z
x : PGame
⊢ x + y ⧏ x + z
[PROOFSTEP]
rw [lf_congr add_comm_equiv add_comm_equiv]
[GOAL]
y z : PGame
h : y ⧏ z
x : PGame
⊢ y + x ⧏ z + x
[PROOFSTEP]
apply add_lf_add_right h
[GOAL]
⊢ star ⧏ 0
[PROOFSTEP]
rw [lf_zero]
[GOAL]
⊢ ∃ j, ∀ (i : LeftMoves (moveRight star j)), moveLeft (moveRight star j) i ⧏ 0
[PROOFSTEP]
use default
[GOAL]
case h
⊢ ∀ (i : LeftMoves (moveRight star default)), moveLeft (moveRight star default) i ⧏ 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
⊢ 0 ⧏ star
[PROOFSTEP]
rw [zero_lf]
[GOAL]
⊢ ∃ i, ∀ (j : RightMoves (moveLeft star i)), 0 ⧏ moveRight (moveLeft star i) j
[PROOFSTEP]
use default
[GOAL]
case h
⊢ ∀ (j : RightMoves (moveLeft star default)), 0 ⧏ moveRight (moveLeft star default) j
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
⊢ -star = star
[PROOFSTEP]
simp [star]