[GOAL]
x : PGame
⊢ Numeric x ↔
    (∀ (i : LeftMoves x) (j : RightMoves x), moveLeft x i < moveRight x j) ∧
      (∀ (i : LeftMoves x), Numeric (moveLeft x i)) ∧ ∀ (j : RightMoves x), Numeric (moveRight x j)
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ Numeric (mk α✝ β✝ a✝¹ a✝) ↔
    (∀ (i : LeftMoves (mk α✝ β✝ a✝¹ a✝)) (j : RightMoves (mk α✝ β✝ a✝¹ a✝)),
        moveLeft (mk α✝ β✝ a✝¹ a✝) i < moveRight (mk α✝ β✝ a✝¹ a✝) j) ∧
      (∀ (i : LeftMoves (mk α✝ β✝ a✝¹ a✝)), Numeric (moveLeft (mk α✝ β✝ a✝¹ a✝) i)) ∧
        ∀ (j : RightMoves (mk α✝ β✝ a✝¹ a✝)), Numeric (moveRight (mk α✝ β✝ a✝¹ a✝) j)
[PROOFSTEP]
rfl
[GOAL]
x : PGame
o : Numeric x
i : LeftMoves x
j : RightMoves x
⊢ moveLeft x i < moveRight x j
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
o : Numeric (PGame.mk α✝ β✝ a✝¹ a✝)
i : LeftMoves (PGame.mk α✝ β✝ a✝¹ a✝)
j : RightMoves (PGame.mk α✝ β✝ a✝¹ a✝)
⊢ moveLeft (PGame.mk α✝ β✝ a✝¹ a✝) i < moveRight (PGame.mk α✝ β✝ a✝¹ a✝) j
[PROOFSTEP]
exact o.1 i j
[GOAL]
x : PGame
o : Numeric x
i : LeftMoves x
⊢ Numeric (PGame.moveLeft x i)
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
o : Numeric (PGame.mk α✝ β✝ a✝¹ a✝)
i : LeftMoves (PGame.mk α✝ β✝ a✝¹ a✝)
⊢ Numeric (PGame.moveLeft (PGame.mk α✝ β✝ a✝¹ a✝) i)
[PROOFSTEP]
exact o.2.1 i
[GOAL]
x : PGame
o : Numeric x
j : RightMoves x
⊢ Numeric (PGame.moveRight x j)
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
o : Numeric (PGame.mk α✝ β✝ a✝¹ a✝)
j : RightMoves (PGame.mk α✝ β✝ a✝¹ a✝)
⊢ Numeric (PGame.moveRight (PGame.mk α✝ β✝ a✝¹ a✝) j)
[PROOFSTEP]
exact o.2.2 j
[GOAL]
x y : PGame
r : x ≡r y
ox : Numeric x
⊢ Numeric y
[PROOFSTEP]
induction' x using PGame.moveRecOn with x IHl IHr generalizing y
[GOAL]
case IH
x✝ y✝ : PGame
r✝ : x✝ ≡r y✝
ox✝ : Numeric x✝
x : PGame
IHl : ∀ (i : LeftMoves x) {y : PGame}, PGame.moveLeft x i ≡r y → Numeric (PGame.moveLeft x i) → Numeric y
IHr : ∀ (j : RightMoves x) {y : PGame}, PGame.moveRight x j ≡r y → Numeric (PGame.moveRight x j) → Numeric y
y : PGame
r : x ≡r y
ox : Numeric x
⊢ Numeric y
[PROOFSTEP]
apply Numeric.mk (fun i j => ?_) (fun i => ?_) fun j => ?_
[GOAL]
x✝ y✝ : PGame
r✝ : x✝ ≡r y✝
ox✝ : Numeric x✝
x : PGame
IHl : ∀ (i : LeftMoves x) {y : PGame}, PGame.moveLeft x i ≡r y → Numeric (PGame.moveLeft x i) → Numeric y
IHr : ∀ (j : RightMoves x) {y : PGame}, PGame.moveRight x j ≡r y → Numeric (PGame.moveRight x j) → Numeric y
y : PGame
r : x ≡r y
ox : Numeric x
i : LeftMoves y
j : RightMoves y
⊢ PGame.moveLeft y i < PGame.moveRight y j
[PROOFSTEP]
rw [← lt_congr (r.moveLeftSymm i).equiv (r.moveRightSymm j).equiv]
[GOAL]
x✝ y✝ : PGame
r✝ : x✝ ≡r y✝
ox✝ : Numeric x✝
x : PGame
IHl : ∀ (i : LeftMoves x) {y : PGame}, PGame.moveLeft x i ≡r y → Numeric (PGame.moveLeft x i) → Numeric y
IHr : ∀ (j : RightMoves x) {y : PGame}, PGame.moveRight x j ≡r y → Numeric (PGame.moveRight x j) → Numeric y
y : PGame
r : x ≡r y
ox : Numeric x
i : LeftMoves y
j : RightMoves y
⊢ PGame.moveLeft x (↑(leftMovesEquiv r).symm i) < PGame.moveRight x (↑(rightMovesEquiv r).symm j)
[PROOFSTEP]
apply ox.left_lt_right
[GOAL]
x✝ y✝ : PGame
r✝ : x✝ ≡r y✝
ox✝ : Numeric x✝
x : PGame
IHl : ∀ (i : LeftMoves x) {y : PGame}, PGame.moveLeft x i ≡r y → Numeric (PGame.moveLeft x i) → Numeric y
IHr : ∀ (j : RightMoves x) {y : PGame}, PGame.moveRight x j ≡r y → Numeric (PGame.moveRight x j) → Numeric y
y : PGame
r : x ≡r y
ox : Numeric x
i : LeftMoves y
⊢ Numeric (PGame.moveLeft y i)
[PROOFSTEP]
exact IHl _ (r.moveLeftSymm i) (ox.moveLeft _)
[GOAL]
x✝ y✝ : PGame
r✝ : x✝ ≡r y✝
ox✝ : Numeric x✝
x : PGame
IHl : ∀ (i : LeftMoves x) {y : PGame}, PGame.moveLeft x i ≡r y → Numeric (PGame.moveLeft x i) → Numeric y
IHr : ∀ (j : RightMoves x) {y : PGame}, PGame.moveRight x j ≡r y → Numeric (PGame.moveRight x j) → Numeric y
y : PGame
r : x ≡r y
ox : Numeric x
j : RightMoves y
⊢ Numeric (PGame.moveRight y j)
[PROOFSTEP]
exact IHr _ (r.moveRightSymm j) (ox.moveRight _)
[GOAL]
x y : PGame
ox : Numeric x
oy : Numeric y
⊢ x ⧏ y → ¬y ⧏ x
[PROOFSTEP]
refine'
  numeric_rec (C := fun x => ∀ z (_oz : Numeric z), x ⧏ z → ¬z ⧏ x) (fun xl xr xL xR hx _oxl _oxr IHxl IHxr => _) x ox y
    oy
[GOAL]
x y : PGame
ox : Numeric x
oy : Numeric y
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), Numeric (xL i)
_oxr : ∀ (i : xr), Numeric (xR i)
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (xR i)
⊢ (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (mk xl xr xL xR)
[PROOFSTEP]
refine' numeric_rec fun yl yr yL yR hy oyl oyr _IHyl _IHyr => _
[GOAL]
x y : PGame
ox : Numeric x
oy : Numeric y
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), Numeric (xL i)
_oxr : ∀ (i : xr), Numeric (xR i)
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), Numeric (yL i)
oyr : ∀ (i : yr), Numeric (yR i)
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ 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
[PROOFSTEP]
rw [mk_lf_mk, mk_lf_mk]
[GOAL]
x y : PGame
ox : Numeric x
oy : Numeric y
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), Numeric (xL i)
_oxr : ∀ (i : xr), Numeric (xR i)
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), Numeric (yL i)
oyr : ∀ (i : yr), Numeric (yR i)
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
⊢ ((∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR) →
    ¬((∃ i, mk yl yr yL yR ≤ xL i) ∨ ∃ j, yR j ≤ mk xl xr xL xR)
[PROOFSTEP]
rintro (⟨i, h₁⟩ | ⟨j, h₁⟩) (⟨i, h₂⟩ | ⟨j, h₂⟩)
[GOAL]
case inl.intro.inl.intro
x y : PGame
ox : Numeric x
oy : Numeric y
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), Numeric (xL i)
_oxr : ∀ (i : xr), Numeric (xR i)
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), Numeric (yL i)
oyr : ∀ (i : yr), Numeric (yR i)
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
i✝ : yl
h₁ : mk xl xr xL xR ≤ yL i✝
i : xl
h₂ : mk yl yr yL yR ≤ xL i
⊢ False
[PROOFSTEP]
exact IHxl _ _ (oyl _) (h₁.moveLeft_lf _) (h₂.moveLeft_lf _)
[GOAL]
case inl.intro.inr.intro
x y : PGame
ox : Numeric x
oy : Numeric y
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), Numeric (xL i)
_oxr : ∀ (i : xr), Numeric (xR i)
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), Numeric (yL i)
oyr : ∀ (i : yr), Numeric (yR i)
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
i : yl
h₁ : mk xl xr xL xR ≤ yL i
j : yr
h₂ : yR j ≤ mk xl xr xL xR
⊢ False
[PROOFSTEP]
exact (le_trans h₂ h₁).not_gf (lf_of_lt (hy _ _))
[GOAL]
case inr.intro.inl.intro
x y : PGame
ox : Numeric x
oy : Numeric y
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), Numeric (xL i)
_oxr : ∀ (i : xr), Numeric (xR i)
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), Numeric (yL i)
oyr : ∀ (i : yr), Numeric (yR i)
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
j : xr
h₁ : xR j ≤ mk yl yr yL yR
i : xl
h₂ : mk yl yr yL yR ≤ xL i
⊢ False
[PROOFSTEP]
exact (le_trans h₁ h₂).not_gf (lf_of_lt (hx _ _))
[GOAL]
case inr.intro.inr.intro
x y : PGame
ox : Numeric x
oy : Numeric y
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), Numeric (xL i)
_oxr : ∀ (i : xr), Numeric (xR i)
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), Numeric z → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), Numeric (yL i)
oyr : ∀ (i : yr), Numeric (yR i)
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
j✝ : xr
h₁ : xR j✝ ≤ mk yl yr yL yR
j : yr
h₂ : yR j ≤ mk xl xr xL xR
⊢ False
[PROOFSTEP]
exact IHxr _ _ (oyr _) (h₁.lf_moveRight _) (h₂.lf_moveRight _)
[GOAL]
x y : PGame
ox : Numeric x
oy : Numeric y
⊢ x ≤ y ↔ (∀ (i : LeftMoves x), moveLeft x i < y) ∧ ∀ (j : RightMoves y), x < moveRight y j
[PROOFSTEP]
refine' le_iff_forall_lf.trans (and_congr _ _)
[GOAL]
case refine'_1
x y : PGame
ox : Numeric x
oy : Numeric y
⊢ (∀ (i : LeftMoves x), moveLeft x i ⧏ y) ↔ ∀ (i : LeftMoves x), moveLeft x i < y
[PROOFSTEP]
refine' forall_congr' fun i => lf_iff_lt _ _
[GOAL]
case refine'_2
x y : PGame
ox : Numeric x
oy : Numeric y
⊢ (∀ (j : RightMoves y), x ⧏ moveRight y j) ↔ ∀ (j : RightMoves y), x < moveRight y j
[PROOFSTEP]
refine' forall_congr' fun i => lf_iff_lt _ _
[GOAL]
case refine'_1.refine'_1
x y : PGame
ox : Numeric x
oy : Numeric y
i : LeftMoves x
⊢ Numeric (moveLeft x i)
[PROOFSTEP]
apply_rules [Numeric.moveLeft, Numeric.moveRight]
[GOAL]
case refine'_1.refine'_2
x y : PGame
ox : Numeric x
oy : Numeric y
i : LeftMoves x
⊢ Numeric y
[PROOFSTEP]
apply_rules [Numeric.moveLeft, Numeric.moveRight]
[GOAL]
case refine'_2.refine'_1
x y : PGame
ox : Numeric x
oy : Numeric y
i : RightMoves y
⊢ Numeric x
[PROOFSTEP]
apply_rules [Numeric.moveLeft, Numeric.moveRight]
[GOAL]
case refine'_2.refine'_2
x y : PGame
ox : Numeric x
oy : Numeric y
i : RightMoves y
⊢ Numeric (moveRight y i)
[PROOFSTEP]
apply_rules [Numeric.moveLeft, Numeric.moveRight]
[GOAL]
x y : PGame
ox : Numeric x
oy : Numeric y
⊢ x < y ↔ (∃ i, x ≤ moveLeft y i) ∨ ∃ j, moveRight x j ≤ y
[PROOFSTEP]
rw [← lf_iff_lt ox oy, lf_iff_exists_le]
[GOAL]
x y : PGame
ox : Numeric x
oy : Numeric y
⊢ 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_lt ox oy, lf_def]
[GOAL]
x y : PGame
ox : Numeric x
oy : Numeric 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') ↔
    (∃ 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]
refine' or_congr _ _
[GOAL]
case refine'_1
x y : PGame
ox : Numeric x
oy : Numeric y
⊢ (∃ i,
      (∀ (i' : LeftMoves x), moveLeft x i' ⧏ moveLeft y i) ∧
        ∀ (j : RightMoves (moveLeft y i)), x ⧏ moveRight (moveLeft y i) j) ↔
    ∃ i,
      (∀ (i' : LeftMoves x), moveLeft x i' < moveLeft y i) ∧
        ∀ (j : RightMoves (moveLeft y i)), x < moveRight (moveLeft y i) j
[PROOFSTEP]
refine' exists_congr fun x_1 => _
[GOAL]
case refine'_2
x y : PGame
ox : Numeric x
oy : Numeric y
⊢ (∃ j,
      (∀ (i : LeftMoves (moveRight x j)), moveLeft (moveRight x j) i ⧏ y) ∧
        ∀ (j' : RightMoves y), moveRight x j ⧏ moveRight y j') ↔
    ∃ j,
      (∀ (i : LeftMoves (moveRight x j)), moveLeft (moveRight x j) i < y) ∧
        ∀ (j' : RightMoves y), moveRight x j < moveRight y j'
[PROOFSTEP]
refine' exists_congr fun x_1 => _
[GOAL]
case refine'_1
x y : PGame
ox : Numeric x
oy : Numeric y
x_1 : LeftMoves y
⊢ ((∀ (i' : LeftMoves x), moveLeft x i' ⧏ moveLeft y x_1) ∧
      ∀ (j : RightMoves (moveLeft y x_1)), x ⧏ moveRight (moveLeft y x_1) j) ↔
    (∀ (i' : LeftMoves x), moveLeft x i' < moveLeft y x_1) ∧
      ∀ (j : RightMoves (moveLeft y x_1)), x < moveRight (moveLeft y x_1) j
[PROOFSTEP]
refine' and_congr _ _
[GOAL]
case refine'_2
x y : PGame
ox : Numeric x
oy : Numeric y
x_1 : RightMoves x
⊢ ((∀ (i : LeftMoves (moveRight x x_1)), moveLeft (moveRight x x_1) i ⧏ y) ∧
      ∀ (j' : RightMoves y), moveRight x x_1 ⧏ moveRight y j') ↔
    (∀ (i : LeftMoves (moveRight x x_1)), moveLeft (moveRight x x_1) i < y) ∧
      ∀ (j' : RightMoves y), moveRight x x_1 < moveRight y j'
[PROOFSTEP]
refine' and_congr _ _
[GOAL]
case refine'_1.refine'_1
x y : PGame
ox : Numeric x
oy : Numeric y
x_1 : LeftMoves y
⊢ (∀ (i' : LeftMoves x), moveLeft x i' ⧏ moveLeft y x_1) ↔ ∀ (i' : LeftMoves x), moveLeft x i' < moveLeft y x_1
[PROOFSTEP]
refine' forall_congr' fun i => lf_iff_lt _ _
[GOAL]
case refine'_1.refine'_2
x y : PGame
ox : Numeric x
oy : Numeric y
x_1 : LeftMoves y
⊢ (∀ (j : RightMoves (moveLeft y x_1)), x ⧏ moveRight (moveLeft y x_1) j) ↔
    ∀ (j : RightMoves (moveLeft y x_1)), x < moveRight (moveLeft y x_1) j
[PROOFSTEP]
refine' forall_congr' fun i => lf_iff_lt _ _
[GOAL]
case refine'_2.refine'_1
x y : PGame
ox : Numeric x
oy : Numeric y
x_1 : RightMoves x
⊢ (∀ (i : LeftMoves (moveRight x x_1)), moveLeft (moveRight x x_1) i ⧏ y) ↔
    ∀ (i : LeftMoves (moveRight x x_1)), moveLeft (moveRight x x_1) i < y
[PROOFSTEP]
refine' forall_congr' fun i => lf_iff_lt _ _
[GOAL]
case refine'_2.refine'_2
x y : PGame
ox : Numeric x
oy : Numeric y
x_1 : RightMoves x
⊢ (∀ (j' : RightMoves y), moveRight x x_1 ⧏ moveRight y j') ↔ ∀ (j' : RightMoves y), moveRight x x_1 < moveRight y j'
[PROOFSTEP]
refine' forall_congr' fun i => lf_iff_lt _ _
[GOAL]
case refine'_1.refine'_1.refine'_1
x y : PGame
ox : Numeric x
oy : Numeric y
x_1 : LeftMoves y
i : LeftMoves x
⊢ Numeric (moveLeft x i)
[PROOFSTEP]
apply_rules [Numeric.moveLeft, Numeric.moveRight]
[GOAL]
case refine'_1.refine'_1.refine'_2
x y : PGame
ox : Numeric x
oy : Numeric y
x_1 : LeftMoves y
i : LeftMoves x
⊢ Numeric (moveLeft y x_1)
[PROOFSTEP]
apply_rules [Numeric.moveLeft, Numeric.moveRight]
[GOAL]
case refine'_1.refine'_2.refine'_1
x y : PGame
ox : Numeric x
oy : Numeric y
x_1 : LeftMoves y
i : RightMoves (moveLeft y x_1)
⊢ Numeric x
[PROOFSTEP]
apply_rules [Numeric.moveLeft, Numeric.moveRight]
[GOAL]
case refine'_1.refine'_2.refine'_2
x y : PGame
ox : Numeric x
oy : Numeric y
x_1 : LeftMoves y
i : RightMoves (moveLeft y x_1)
⊢ Numeric (moveRight (moveLeft y x_1) i)
[PROOFSTEP]
apply_rules [Numeric.moveLeft, Numeric.moveRight]
[GOAL]
case refine'_2.refine'_1.refine'_1
x y : PGame
ox : Numeric x
oy : Numeric y
x_1 : RightMoves x
i : LeftMoves (moveRight x x_1)
⊢ Numeric (moveLeft (moveRight x x_1) i)
[PROOFSTEP]
apply_rules [Numeric.moveLeft, Numeric.moveRight]
[GOAL]
case refine'_2.refine'_1.refine'_2
x y : PGame
ox : Numeric x
oy : Numeric y
x_1 : RightMoves x
i : LeftMoves (moveRight x x_1)
⊢ Numeric y
[PROOFSTEP]
apply_rules [Numeric.moveLeft, Numeric.moveRight]
[GOAL]
case refine'_2.refine'_2.refine'_1
x y : PGame
ox : Numeric x
oy : Numeric y
x_1 : RightMoves x
i : RightMoves y
⊢ Numeric (moveRight x x_1)
[PROOFSTEP]
apply_rules [Numeric.moveLeft, Numeric.moveRight]
[GOAL]
case refine'_2.refine'_2.refine'_2
x y : PGame
ox : Numeric x
oy : Numeric y
x_1 : RightMoves x
i : RightMoves y
⊢ Numeric (moveRight y i)
[PROOFSTEP]
apply_rules [Numeric.moveLeft, Numeric.moveRight]
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
⊢ ∀ (i : xl ⊕ yl) (j : xr ⊕ yr),
    (fun t =>
          Sum.rec
            (fun i =>
              (fun a =>
                  rec (motive := fun x => PGame → PGame)
                    (fun xl xr a a IHxl IHxr y =>
                      rec
                        (fun yl yr yL yR IHyl IHyr =>
                          let_fun y := PGame.mk yl yr yL yR;
                          PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                            Sum.rec (fun i => IHxr i y) IHyr t)
                        y)
                    (xL a))
                i (PGame.mk yl yr yL yR))
            (fun a =>
              rec
                (fun yl yr yL yR IHyl IHyr =>
                  let_fun y := PGame.mk yl yr yL yR;
                  PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                    (fun t =>
                      Sum.rec
                        (fun i =>
                          (fun a =>
                              rec (motive := fun x => PGame → PGame)
                                (fun xl xr a a IHxl IHxr y =>
                                  rec
                                    (fun yl yr yL yR IHyl IHyr =>
                                      let_fun y := PGame.mk yl yr yL yR;
                                      PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t)
                                        fun t => Sum.rec (fun i => IHxr i y) IHyr t)
                                    y)
                                (xL a))
                            i y)
                        IHyl t)
                    fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xR a))
                          i y)
                      IHyr t)
                (yL a))
            t)
        i <
      (fun t =>
          Sum.rec
            (fun i =>
              (fun a =>
                  rec (motive := fun x => PGame → PGame)
                    (fun xl xr a a IHxl IHxr y =>
                      rec
                        (fun yl yr yL yR IHyl IHyr =>
                          let_fun y := PGame.mk yl yr yL yR;
                          PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                            Sum.rec (fun i => IHxr i y) IHyr t)
                        y)
                    (xR a))
                i (PGame.mk yl yr yL yR))
            (fun a =>
              rec
                (fun yl yr yL yR IHyl IHyr =>
                  let_fun y := PGame.mk yl yr yL yR;
                  PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                    (fun t =>
                      Sum.rec
                        (fun i =>
                          (fun a =>
                              rec (motive := fun x => PGame → PGame)
                                (fun xl xr a a IHxl IHxr y =>
                                  rec
                                    (fun yl yr yL yR IHyl IHyr =>
                                      let_fun y := PGame.mk yl yr yL yR;
                                      PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t)
                                        fun t => Sum.rec (fun i => IHxr i y) IHyr t)
                                    y)
                                (xL a))
                            i y)
                        IHyl t)
                    fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xR a))
                          i y)
                      IHyr t)
                (yR a))
            t)
        j
[PROOFSTEP]
rintro (ix | iy) (jx | jy)
[GOAL]
case inl.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
ix : xl
jx : xr
⊢ (fun t =>
        Sum.rec
          (fun i =>
            (fun a =>
                rec (motive := fun x => PGame → PGame)
                  (fun xl xr a a IHxl IHxr y =>
                    rec
                      (fun yl yr yL yR IHyl IHyr =>
                        let_fun y := PGame.mk yl yr yL yR;
                        PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                          Sum.rec (fun i => IHxr i y) IHyr t)
                      y)
                  (xL a))
              i (PGame.mk yl yr yL yR))
          (fun a =>
            rec
              (fun yl yr yL yR IHyl IHyr =>
                let_fun y := PGame.mk yl yr yL yR;
                PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                  (fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xL a))
                          i y)
                      IHyl t)
                  fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := PGame.mk yl yr yL yR;
                                  PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xR a))
                        i y)
                    IHyr t)
              (yL a))
          t)
      (Sum.inl ix) <
    (fun t =>
        Sum.rec
          (fun i =>
            (fun a =>
                rec (motive := fun x => PGame → PGame)
                  (fun xl xr a a IHxl IHxr y =>
                    rec
                      (fun yl yr yL yR IHyl IHyr =>
                        let_fun y := PGame.mk yl yr yL yR;
                        PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                          Sum.rec (fun i => IHxr i y) IHyr t)
                      y)
                  (xR a))
              i (PGame.mk yl yr yL yR))
          (fun a =>
            rec
              (fun yl yr yL yR IHyl IHyr =>
                let_fun y := PGame.mk yl yr yL yR;
                PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                  (fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xL a))
                          i y)
                      IHyl t)
                  fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := PGame.mk yl yr yL yR;
                                  PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xR a))
                        i y)
                    IHyr t)
              (yR a))
          t)
      (Sum.inl jx)
[PROOFSTEP]
exact add_lt_add_right (ox.1 ix jx) _
[GOAL]
case inl.inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
ix : xl
jy : yr
⊢ (fun t =>
        Sum.rec
          (fun i =>
            (fun a =>
                rec (motive := fun x => PGame → PGame)
                  (fun xl xr a a IHxl IHxr y =>
                    rec
                      (fun yl yr yL yR IHyl IHyr =>
                        let_fun y := PGame.mk yl yr yL yR;
                        PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                          Sum.rec (fun i => IHxr i y) IHyr t)
                      y)
                  (xL a))
              i (PGame.mk yl yr yL yR))
          (fun a =>
            rec
              (fun yl yr yL yR IHyl IHyr =>
                let_fun y := PGame.mk yl yr yL yR;
                PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                  (fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xL a))
                          i y)
                      IHyl t)
                  fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := PGame.mk yl yr yL yR;
                                  PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xR a))
                        i y)
                    IHyr t)
              (yL a))
          t)
      (Sum.inl ix) <
    (fun t =>
        Sum.rec
          (fun i =>
            (fun a =>
                rec (motive := fun x => PGame → PGame)
                  (fun xl xr a a IHxl IHxr y =>
                    rec
                      (fun yl yr yL yR IHyl IHyr =>
                        let_fun y := PGame.mk yl yr yL yR;
                        PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                          Sum.rec (fun i => IHxr i y) IHyr t)
                      y)
                  (xR a))
              i (PGame.mk yl yr yL yR))
          (fun a =>
            rec
              (fun yl yr yL yR IHyl IHyr =>
                let_fun y := PGame.mk yl yr yL yR;
                PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                  (fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xL a))
                          i y)
                      IHyl t)
                  fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := PGame.mk yl yr yL yR;
                                  PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xR a))
                        i y)
                    IHyr t)
              (yR a))
          t)
      (Sum.inr jy)
[PROOFSTEP]
exact
  (add_lf_add_of_lf_of_le (lf_mk _ _ ix) (oy.le_moveRight jy)).lt ((ox.moveLeft ix).add oy) (ox.add (oy.moveRight jy))
[GOAL]
case inr.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
iy : yl
jx : xr
⊢ (fun t =>
        Sum.rec
          (fun i =>
            (fun a =>
                rec (motive := fun x => PGame → PGame)
                  (fun xl xr a a IHxl IHxr y =>
                    rec
                      (fun yl yr yL yR IHyl IHyr =>
                        let_fun y := PGame.mk yl yr yL yR;
                        PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                          Sum.rec (fun i => IHxr i y) IHyr t)
                      y)
                  (xL a))
              i (PGame.mk yl yr yL yR))
          (fun a =>
            rec
              (fun yl yr yL yR IHyl IHyr =>
                let_fun y := PGame.mk yl yr yL yR;
                PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                  (fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xL a))
                          i y)
                      IHyl t)
                  fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := PGame.mk yl yr yL yR;
                                  PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xR a))
                        i y)
                    IHyr t)
              (yL a))
          t)
      (Sum.inr iy) <
    (fun t =>
        Sum.rec
          (fun i =>
            (fun a =>
                rec (motive := fun x => PGame → PGame)
                  (fun xl xr a a IHxl IHxr y =>
                    rec
                      (fun yl yr yL yR IHyl IHyr =>
                        let_fun y := PGame.mk yl yr yL yR;
                        PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                          Sum.rec (fun i => IHxr i y) IHyr t)
                      y)
                  (xR a))
              i (PGame.mk yl yr yL yR))
          (fun a =>
            rec
              (fun yl yr yL yR IHyl IHyr =>
                let_fun y := PGame.mk yl yr yL yR;
                PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                  (fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xL a))
                          i y)
                      IHyl t)
                  fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := PGame.mk yl yr yL yR;
                                  PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xR a))
                        i y)
                    IHyr t)
              (yR a))
          t)
      (Sum.inl jx)
[PROOFSTEP]
exact
  (add_lf_add_of_lf_of_le (mk_lf _ _ jx) (oy.moveLeft_le iy)).lt (ox.add (oy.moveLeft iy)) ((ox.moveRight jx).add oy)
[GOAL]
case inr.inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
iy : yl
jy : yr
⊢ (fun t =>
        Sum.rec
          (fun i =>
            (fun a =>
                rec (motive := fun x => PGame → PGame)
                  (fun xl xr a a IHxl IHxr y =>
                    rec
                      (fun yl yr yL yR IHyl IHyr =>
                        let_fun y := PGame.mk yl yr yL yR;
                        PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                          Sum.rec (fun i => IHxr i y) IHyr t)
                      y)
                  (xL a))
              i (PGame.mk yl yr yL yR))
          (fun a =>
            rec
              (fun yl yr yL yR IHyl IHyr =>
                let_fun y := PGame.mk yl yr yL yR;
                PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                  (fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xL a))
                          i y)
                      IHyl t)
                  fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := PGame.mk yl yr yL yR;
                                  PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xR a))
                        i y)
                    IHyr t)
              (yL a))
          t)
      (Sum.inr iy) <
    (fun t =>
        Sum.rec
          (fun i =>
            (fun a =>
                rec (motive := fun x => PGame → PGame)
                  (fun xl xr a a IHxl IHxr y =>
                    rec
                      (fun yl yr yL yR IHyl IHyr =>
                        let_fun y := PGame.mk yl yr yL yR;
                        PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                          Sum.rec (fun i => IHxr i y) IHyr t)
                      y)
                  (xR a))
              i (PGame.mk yl yr yL yR))
          (fun a =>
            rec
              (fun yl yr yL yR IHyl IHyr =>
                let_fun y := PGame.mk yl yr yL yR;
                PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                  (fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xL a))
                          i y)
                      IHyl t)
                  fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := PGame.mk yl yr yL yR;
                                  PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xR a))
                        i y)
                    IHyr t)
              (yR a))
          t)
      (Sum.inr jy)
[PROOFSTEP]
exact add_lt_add_left (oy.1 iy jy) ⟨xl, xr, xL, xR⟩
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
⊢ (∀ (i : xl ⊕ yl),
      Numeric
        ((fun t =>
            Sum.rec
              (fun i =>
                (fun a =>
                    rec (motive := fun x => PGame → PGame)
                      (fun xl xr a a IHxl IHxr y =>
                        rec
                          (fun yl yr yL yR IHyl IHyr =>
                            let_fun y := PGame.mk yl yr yL yR;
                            PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                              Sum.rec (fun i => IHxr i y) IHyr t)
                          y)
                      (xL a))
                  i (PGame.mk yl yr yL yR))
              (fun a =>
                rec
                  (fun yl yr yL yR IHyl IHyr =>
                    let_fun y := PGame.mk yl yr yL yR;
                    PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                      (fun t =>
                        Sum.rec
                          (fun i =>
                            (fun a =>
                                rec (motive := fun x => PGame → PGame)
                                  (fun xl xr a a IHxl IHxr y =>
                                    rec
                                      (fun yl yr yL yR IHyl IHyr =>
                                        let_fun y := PGame.mk yl yr yL yR;
                                        PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t)
                                          fun t => Sum.rec (fun i => IHxr i y) IHyr t)
                                      y)
                                  (xL a))
                              i y)
                          IHyl t)
                      fun t =>
                      Sum.rec
                        (fun i =>
                          (fun a =>
                              rec (motive := fun x => PGame → PGame)
                                (fun xl xr a a IHxl IHxr y =>
                                  rec
                                    (fun yl yr yL yR IHyl IHyr =>
                                      let_fun y := PGame.mk yl yr yL yR;
                                      PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t)
                                        fun t => Sum.rec (fun i => IHxr i y) IHyr t)
                                    y)
                                (xR a))
                            i y)
                        IHyr t)
                  (yL a))
              t)
          i)) ∧
    ∀ (j : xr ⊕ yr),
      Numeric
        ((fun t =>
            Sum.rec
              (fun i =>
                (fun a =>
                    rec (motive := fun x => PGame → PGame)
                      (fun xl xr a a IHxl IHxr y =>
                        rec
                          (fun yl yr yL yR IHyl IHyr =>
                            let_fun y := PGame.mk yl yr yL yR;
                            PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                              Sum.rec (fun i => IHxr i y) IHyr t)
                          y)
                      (xR a))
                  i (PGame.mk yl yr yL yR))
              (fun a =>
                rec
                  (fun yl yr yL yR IHyl IHyr =>
                    let_fun y := PGame.mk yl yr yL yR;
                    PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                      (fun t =>
                        Sum.rec
                          (fun i =>
                            (fun a =>
                                rec (motive := fun x => PGame → PGame)
                                  (fun xl xr a a IHxl IHxr y =>
                                    rec
                                      (fun yl yr yL yR IHyl IHyr =>
                                        let_fun y := PGame.mk yl yr yL yR;
                                        PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t)
                                          fun t => Sum.rec (fun i => IHxr i y) IHyr t)
                                      y)
                                  (xL a))
                              i y)
                          IHyl t)
                      fun t =>
                      Sum.rec
                        (fun i =>
                          (fun a =>
                              rec (motive := fun x => PGame → PGame)
                                (fun xl xr a a IHxl IHxr y =>
                                  rec
                                    (fun yl yr yL yR IHyl IHyr =>
                                      let_fun y := PGame.mk yl yr yL yR;
                                      PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t)
                                        fun t => Sum.rec (fun i => IHxr i y) IHyr t)
                                    y)
                                (xR a))
                            i y)
                        IHyr t)
                  (yR a))
              t)
          j)
[PROOFSTEP]
constructor
[GOAL]
case left
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
⊢ ∀ (i : xl ⊕ yl),
    Numeric
      ((fun t =>
          Sum.rec
            (fun i =>
              (fun a =>
                  rec (motive := fun x => PGame → PGame)
                    (fun xl xr a a IHxl IHxr y =>
                      rec
                        (fun yl yr yL yR IHyl IHyr =>
                          let_fun y := PGame.mk yl yr yL yR;
                          PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                            Sum.rec (fun i => IHxr i y) IHyr t)
                        y)
                    (xL a))
                i (PGame.mk yl yr yL yR))
            (fun a =>
              rec
                (fun yl yr yL yR IHyl IHyr =>
                  let_fun y := PGame.mk yl yr yL yR;
                  PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                    (fun t =>
                      Sum.rec
                        (fun i =>
                          (fun a =>
                              rec (motive := fun x => PGame → PGame)
                                (fun xl xr a a IHxl IHxr y =>
                                  rec
                                    (fun yl yr yL yR IHyl IHyr =>
                                      let_fun y := PGame.mk yl yr yL yR;
                                      PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t)
                                        fun t => Sum.rec (fun i => IHxr i y) IHyr t)
                                    y)
                                (xL a))
                            i y)
                        IHyl t)
                    fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xR a))
                          i y)
                      IHyr t)
                (yL a))
            t)
        i)
[PROOFSTEP]
rintro (ix | iy)
[GOAL]
case left.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
ix : xl
⊢ Numeric
    ((fun t =>
        Sum.rec
          (fun i =>
            (fun a =>
                rec (motive := fun x => PGame → PGame)
                  (fun xl xr a a IHxl IHxr y =>
                    rec
                      (fun yl yr yL yR IHyl IHyr =>
                        let_fun y := PGame.mk yl yr yL yR;
                        PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                          Sum.rec (fun i => IHxr i y) IHyr t)
                      y)
                  (xL a))
              i (PGame.mk yl yr yL yR))
          (fun a =>
            rec
              (fun yl yr yL yR IHyl IHyr =>
                let_fun y := PGame.mk yl yr yL yR;
                PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                  (fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xL a))
                          i y)
                      IHyl t)
                  fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := PGame.mk yl yr yL yR;
                                  PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xR a))
                        i y)
                    IHyr t)
              (yL a))
          t)
      (Sum.inl ix))
[PROOFSTEP]
exact (ox.moveLeft ix).add oy
[GOAL]
case left.inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
iy : yl
⊢ Numeric
    ((fun t =>
        Sum.rec
          (fun i =>
            (fun a =>
                rec (motive := fun x => PGame → PGame)
                  (fun xl xr a a IHxl IHxr y =>
                    rec
                      (fun yl yr yL yR IHyl IHyr =>
                        let_fun y := PGame.mk yl yr yL yR;
                        PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                          Sum.rec (fun i => IHxr i y) IHyr t)
                      y)
                  (xL a))
              i (PGame.mk yl yr yL yR))
          (fun a =>
            rec
              (fun yl yr yL yR IHyl IHyr =>
                let_fun y := PGame.mk yl yr yL yR;
                PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                  (fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xL a))
                          i y)
                      IHyl t)
                  fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := PGame.mk yl yr yL yR;
                                  PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xR a))
                        i y)
                    IHyr t)
              (yL a))
          t)
      (Sum.inr iy))
[PROOFSTEP]
exact ox.add (oy.moveLeft iy)
[GOAL]
case right
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
⊢ ∀ (j : xr ⊕ yr),
    Numeric
      ((fun t =>
          Sum.rec
            (fun i =>
              (fun a =>
                  rec (motive := fun x => PGame → PGame)
                    (fun xl xr a a IHxl IHxr y =>
                      rec
                        (fun yl yr yL yR IHyl IHyr =>
                          let_fun y := PGame.mk yl yr yL yR;
                          PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                            Sum.rec (fun i => IHxr i y) IHyr t)
                        y)
                    (xR a))
                i (PGame.mk yl yr yL yR))
            (fun a =>
              rec
                (fun yl yr yL yR IHyl IHyr =>
                  let_fun y := PGame.mk yl yr yL yR;
                  PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                    (fun t =>
                      Sum.rec
                        (fun i =>
                          (fun a =>
                              rec (motive := fun x => PGame → PGame)
                                (fun xl xr a a IHxl IHxr y =>
                                  rec
                                    (fun yl yr yL yR IHyl IHyr =>
                                      let_fun y := PGame.mk yl yr yL yR;
                                      PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t)
                                        fun t => Sum.rec (fun i => IHxr i y) IHyr t)
                                    y)
                                (xL a))
                            i y)
                        IHyl t)
                    fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xR a))
                          i y)
                      IHyr t)
                (yR a))
            t)
        j)
[PROOFSTEP]
rintro (jx | jy)
[GOAL]
case right.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
jx : xr
⊢ Numeric
    ((fun t =>
        Sum.rec
          (fun i =>
            (fun a =>
                rec (motive := fun x => PGame → PGame)
                  (fun xl xr a a IHxl IHxr y =>
                    rec
                      (fun yl yr yL yR IHyl IHyr =>
                        let_fun y := PGame.mk yl yr yL yR;
                        PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                          Sum.rec (fun i => IHxr i y) IHyr t)
                      y)
                  (xR a))
              i (PGame.mk yl yr yL yR))
          (fun a =>
            rec
              (fun yl yr yL yR IHyl IHyr =>
                let_fun y := PGame.mk yl yr yL yR;
                PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                  (fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xL a))
                          i y)
                      IHyl t)
                  fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := PGame.mk yl yr yL yR;
                                  PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xR a))
                        i y)
                    IHyr t)
              (yR a))
          t)
      (Sum.inl jx))
[PROOFSTEP]
apply (ox.moveRight jx).add oy
[GOAL]
case right.inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
jy : yr
⊢ Numeric
    ((fun t =>
        Sum.rec
          (fun i =>
            (fun a =>
                rec (motive := fun x => PGame → PGame)
                  (fun xl xr a a IHxl IHxr y =>
                    rec
                      (fun yl yr yL yR IHyl IHyr =>
                        let_fun y := PGame.mk yl yr yL yR;
                        PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                          Sum.rec (fun i => IHxr i y) IHyr t)
                      y)
                  (xR a))
              i (PGame.mk yl yr yL yR))
          (fun a =>
            rec
              (fun yl yr yL yR IHyl IHyr =>
                let_fun y := PGame.mk yl yr yL yR;
                PGame.mk (xl ⊕ yl) (xr ⊕ yr)
                  (fun t =>
                    Sum.rec
                      (fun i =>
                        (fun a =>
                            rec (motive := fun x => PGame → PGame)
                              (fun xl xr a a IHxl IHxr y =>
                                rec
                                  (fun yl yr yL yR IHyl IHyr =>
                                    let_fun y := PGame.mk yl yr yL yR;
                                    PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                      Sum.rec (fun i => IHxr i y) IHyr t)
                                  y)
                              (xL a))
                          i y)
                      IHyl t)
                  fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := PGame.mk yl yr yL yR;
                                  PGame.mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xR a))
                        i y)
                    IHyr t)
              (yR a))
          t)
      (Sum.inr jy))
[PROOFSTEP]
apply ox.add (oy.moveRight jy)
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Numeric x) ×' Numeric x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
            Prod.instWellFoundedRelationProd).1
        y { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } } →
      Numeric (y.1 + y.2.1)
ix : xl
⊢ (invImage
        (fun a =>
          PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
        Prod.instWellFoundedRelationProd).1
    { fst := PGame.moveLeft (PGame.mk xl xr xL xR) ix,
      snd :=
        { fst := PGame.mk yl yr yL yR,
          snd := { fst := (_ : Numeric (PGame.moveLeft (PGame.mk xl xr xL xR) ix)), snd := oy } } }
    { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Numeric x) ×' Numeric x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
            Prod.instWellFoundedRelationProd).1
        y { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } } →
      Numeric (y.1 + y.2.1)
jy : yr
⊢ (invImage
        (fun a =>
          PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
        Prod.instWellFoundedRelationProd).1
    { fst := PGame.mk xl xr xL xR,
      snd :=
        { fst := PGame.moveRight (PGame.mk yl yr yL yR) jy,
          snd := { fst := ox, snd := (_ : Numeric (PGame.moveRight (PGame.mk yl yr yL yR) jy)) } } }
    { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Numeric x) ×' Numeric x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
            Prod.instWellFoundedRelationProd).1
        y { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } } →
      Numeric (y.1 + y.2.1)
iy : yl
⊢ (invImage
        (fun a =>
          PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
        Prod.instWellFoundedRelationProd).1
    { fst := PGame.mk xl xr xL xR,
      snd :=
        { fst := PGame.moveLeft (PGame.mk yl yr yL yR) iy,
          snd := { fst := ox, snd := (_ : Numeric (PGame.moveLeft (PGame.mk yl yr yL yR) iy)) } } }
    { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Numeric x) ×' Numeric x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
            Prod.instWellFoundedRelationProd).1
        y { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } } →
      Numeric (y.1 + y.2.1)
jx : xr
⊢ (invImage
        (fun a =>
          PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
        Prod.instWellFoundedRelationProd).1
    { fst := PGame.moveRight (PGame.mk xl xr xL xR) jx,
      snd :=
        { fst := PGame.mk yl yr yL yR,
          snd := { fst := (_ : Numeric (PGame.moveRight (PGame.mk xl xr xL xR) jx)), snd := oy } } }
    { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Numeric x) ×' Numeric x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
            Prod.instWellFoundedRelationProd).1
        y { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } } →
      Numeric (y.1 + y.2.1)
ix : xl
⊢ (invImage
        (fun a =>
          PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
        Prod.instWellFoundedRelationProd).1
    { fst := PGame.moveLeft (PGame.mk xl xr xL xR) ix,
      snd :=
        { fst := PGame.mk yl yr yL yR,
          snd := { fst := (_ : Numeric (PGame.moveLeft (PGame.mk xl xr xL xR) ix)), snd := oy } } }
    { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Numeric x) ×' Numeric x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
            Prod.instWellFoundedRelationProd).1
        y { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } } →
      Numeric (y.1 + y.2.1)
iy : yl
⊢ (invImage
        (fun a =>
          PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
        Prod.instWellFoundedRelationProd).1
    { fst := PGame.mk xl xr xL xR,
      snd := { fst := yL iy, snd := { fst := ox, snd := (_ : Numeric (PGame.moveLeft (PGame.mk yl yr yL yR) iy)) } } }
    { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Numeric x) ×' Numeric x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
            Prod.instWellFoundedRelationProd).1
        y { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } } →
      Numeric (y.1 + y.2.1)
jx : xr
⊢ (invImage
        (fun a =>
          PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
        Prod.instWellFoundedRelationProd).1
    { fst := PGame.moveRight (PGame.mk xl xr xL xR) jx,
      snd :=
        { fst := PGame.mk yl yr yL yR,
          snd := { fst := (_ : Numeric (PGame.moveRight (PGame.mk xl xr xL xR) jx)), snd := oy } } }
    { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : Numeric (PGame.mk xl xr xL xR)
oy : Numeric (PGame.mk yl yr yL yR)
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Numeric x) ×' Numeric x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
            Prod.instWellFoundedRelationProd).1
        y { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } } →
      Numeric (y.1 + y.2.1)
jy : yr
⊢ (invImage
        (fun a =>
          PSigma.casesOn a fun x snd => PSigma.casesOn snd fun y snd => PSigma.casesOn snd fun x_1 snd => (x, y))
        Prod.instWellFoundedRelationProd).1
    { fst := PGame.mk xl xr xL xR,
      snd :=
        { fst := PGame.moveRight (PGame.mk yl yr yL yR) jy,
          snd := { fst := ox, snd := (_ : Numeric (PGame.moveRight (PGame.mk yl yr yL yR) jy)) } } }
    { fst := PGame.mk xl xr xL xR, snd := { fst := PGame.mk yl yr yL yR, snd := { fst := ox, snd := oy } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
o : Ordinal.{u_1}
⊢ Numeric (Ordinal.toPGame o)
[PROOFSTEP]
induction' o using Ordinal.induction with o IH
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → Numeric (Ordinal.toPGame k)
⊢ Numeric (Ordinal.toPGame o)
[PROOFSTEP]
apply numeric_of_isEmpty_rightMoves
[GOAL]
case h.H
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → Numeric (Ordinal.toPGame k)
⊢ ∀ (i : LeftMoves (Ordinal.toPGame o)), Numeric (moveLeft (Ordinal.toPGame o) i)
[PROOFSTEP]
simpa using fun i => IH _ (Ordinal.toLeftMovesToPGame_symm_lt i)
[GOAL]
⊢ ∀ (a b c : Surreal), a + b + c = a + (b + c)
[PROOFSTEP]
rintro ⟨_⟩ ⟨_⟩ ⟨_⟩
[GOAL]
case mk.mk.mk
a✝³ : Surreal
a✝² : Subtype Numeric
b✝ : Surreal
a✝¹ : Subtype Numeric
c✝ : Surreal
a✝ : Subtype Numeric
⊢ Quot.mk Setoid.r a✝² + Quot.mk Setoid.r a✝¹ + Quot.mk Setoid.r a✝ =
    Quot.mk Setoid.r a✝² + (Quot.mk Setoid.r a✝¹ + Quot.mk Setoid.r a✝)
[PROOFSTEP]
exact Quotient.sound add_assoc_equiv
[GOAL]
⊢ ∀ (a : Surreal), 0 + a = a
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
a✝ : Surreal
a : Subtype Numeric
⊢ 0 + Quot.mk Setoid.r a = Quot.mk Setoid.r a
[PROOFSTEP]
exact Quotient.sound (zero_add_equiv a)
[GOAL]
⊢ ∀ (a : Surreal), a + 0 = a
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
a✝ : Surreal
a : Subtype Numeric
⊢ Quot.mk Setoid.r a + 0 = Quot.mk Setoid.r a
[PROOFSTEP]
exact Quotient.sound (add_zero_equiv a)
[GOAL]
⊢ ∀ (a : Surreal), -a + a = 0
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
a✝ : Surreal
a : Subtype Numeric
⊢ -Quot.mk Setoid.r a + Quot.mk Setoid.r a = 0
[PROOFSTEP]
exact Quotient.sound (add_left_neg_equiv a)
[GOAL]
⊢ ∀ (a b : Surreal), a + b = b + a
[PROOFSTEP]
rintro ⟨_⟩ ⟨_⟩
[GOAL]
case mk.mk
a✝² : Surreal
a✝¹ : Subtype Numeric
b✝ : Surreal
a✝ : Subtype Numeric
⊢ Quot.mk Setoid.r a✝¹ + Quot.mk Setoid.r a✝ = Quot.mk Setoid.r a✝ + Quot.mk Setoid.r a✝¹
[PROOFSTEP]
exact Quotient.sound add_comm_equiv
[GOAL]
⊢ ∀ (a : Surreal), a ≤ a
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case mk
a✝¹ : Surreal
a✝ : Subtype Numeric
⊢ Quot.mk Setoid.r a✝ ≤ Quot.mk Setoid.r a✝
[PROOFSTEP]
apply @le_rfl PGame
[GOAL]
⊢ ∀ (a b c : Surreal), a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
rintro ⟨_⟩ ⟨_⟩ ⟨_⟩
[GOAL]
case mk.mk.mk
a✝³ : Surreal
a✝² : Subtype Numeric
b✝ : Surreal
a✝¹ : Subtype Numeric
c✝ : Surreal
a✝ : Subtype Numeric
⊢ Quot.mk Setoid.r a✝² ≤ Quot.mk Setoid.r a✝¹ →
    Quot.mk Setoid.r a✝¹ ≤ Quot.mk Setoid.r a✝ → Quot.mk Setoid.r a✝² ≤ Quot.mk Setoid.r a✝
[PROOFSTEP]
apply @le_trans PGame
[GOAL]
⊢ ∀ (a b : Surreal), a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
rintro ⟨_, ox⟩ ⟨_, oy⟩
[GOAL]
case mk.mk.mk.mk
a✝ : Surreal
val✝¹ : PGame
ox : Numeric val✝¹
b✝ : Surreal
val✝ : PGame
oy : Numeric val✝
⊢ Quot.mk Setoid.r { val := val✝¹, property := ox } < Quot.mk Setoid.r { val := val✝, property := oy } ↔
    Quot.mk Setoid.r { val := val✝¹, property := ox } ≤ Quot.mk Setoid.r { val := val✝, property := oy } ∧
      ¬Quot.mk Setoid.r { val := val✝, property := oy } ≤ Quot.mk Setoid.r { val := val✝¹, property := ox }
[PROOFSTEP]
apply @lt_iff_le_not_le PGame
[GOAL]
⊢ ∀ (a b : Surreal), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
rintro ⟨_⟩ ⟨_⟩ h₁ h₂
[GOAL]
case mk.mk
a✝² : Surreal
a✝¹ : Subtype Numeric
b✝ : Surreal
a✝ : Subtype Numeric
h₁ : Quot.mk Setoid.r a✝¹ ≤ Quot.mk Setoid.r a✝
h₂ : Quot.mk Setoid.r a✝ ≤ Quot.mk Setoid.r a✝¹
⊢ Quot.mk Setoid.r a✝¹ = Quot.mk Setoid.r a✝
[PROOFSTEP]
exact Quotient.sound ⟨h₁, h₂⟩
[GOAL]
⊢ ∀ (a b : Surreal), a ≤ b → ∀ (c : Surreal), c + a ≤ c + b
[PROOFSTEP]
rintro ⟨_⟩ ⟨_⟩ hx ⟨_⟩
[GOAL]
case mk.mk.mk
a✝³ : Surreal
a✝² : Subtype Numeric
b✝ : Surreal
a✝¹ : Subtype Numeric
hx : Quot.mk Setoid.r a✝² ≤ Quot.mk Setoid.r a✝¹
c✝ : Surreal
a✝ : Subtype Numeric
⊢ Quot.mk Setoid.r a✝ + Quot.mk Setoid.r a✝² ≤ Quot.mk Setoid.r a✝ + Quot.mk Setoid.r a✝¹
[PROOFSTEP]
exact @add_le_add_left PGame _ _ _ _ _ hx _
[GOAL]
src✝ : OrderedAddCommGroup Surreal := orderedAddCommGroup
⊢ ∀ (a b : Surreal), a ≤ b ∨ b ≤ a
[PROOFSTEP]
rintro ⟨⟨x, ox⟩⟩ ⟨⟨y, oy⟩⟩
[GOAL]
case mk.mk.mk.mk
src✝ : OrderedAddCommGroup Surreal := orderedAddCommGroup
a✝ : Surreal
x : PGame
ox : Numeric x
b✝ : Surreal
y : PGame
oy : Numeric y
⊢ Quot.mk Setoid.r { val := x, property := ox } ≤ Quot.mk Setoid.r { val := y, property := oy } ∨
    Quot.mk Setoid.r { val := y, property := oy } ≤ Quot.mk Setoid.r { val := x, property := ox }
[PROOFSTEP]
exact or_iff_not_imp_left.2 fun h => (PGame.not_le.1 h).le oy ox
[GOAL]
⊢ ∀ (x y : Surreal),
    ZeroHom.toFun
        {
          toFun :=
            lift (fun x x_1 => Quotient.mk setoid x)
              (_ :
                ∀ {x y : PGame},
                  Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
          map_zero' :=
            (_ :
              lift (fun x x_1 => Quotient.mk setoid x)
                  (_ :
                    ∀ {x y : PGame},
                      Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                  0 =
                lift (fun x x_1 => Quotient.mk setoid x)
                  (_ :
                    ∀ {x y : PGame},
                      Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                  0) }
        (x + y) =
      ZeroHom.toFun
          {
            toFun :=
              lift (fun x x_1 => Quotient.mk setoid x)
                (_ :
                  ∀ {x y : PGame},
                    Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
            map_zero' :=
              (_ :
                lift (fun x x_1 => Quotient.mk setoid x)
                    (_ :
                      ∀ {x y : PGame},
                        Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                    0 =
                  lift (fun x x_1 => Quotient.mk setoid x)
                    (_ :
                      ∀ {x y : PGame},
                        Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                    0) }
          x +
        ZeroHom.toFun
          {
            toFun :=
              lift (fun x x_1 => Quotient.mk setoid x)
                (_ :
                  ∀ {x y : PGame},
                    Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
            map_zero' :=
              (_ :
                lift (fun x x_1 => Quotient.mk setoid x)
                    (_ :
                      ∀ {x y : PGame},
                        Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                    0 =
                  lift (fun x x_1 => Quotient.mk setoid x)
                    (_ :
                      ∀ {x y : PGame},
                        Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                    0) }
          y
[PROOFSTEP]
rintro ⟨_, _⟩ ⟨_, _⟩
[GOAL]
case mk.mk.mk.mk
x✝ : Surreal
val✝¹ : PGame
property✝¹ : Numeric val✝¹
y✝ : Surreal
val✝ : PGame
property✝ : Numeric val✝
⊢ ZeroHom.toFun
      {
        toFun :=
          lift (fun x x_1 => Quotient.mk setoid x)
            (_ :
              ∀ {x y : PGame}, Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
        map_zero' :=
          (_ :
            lift (fun x x_1 => Quotient.mk setoid x)
                (_ :
                  ∀ {x y : PGame},
                    Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                0 =
              lift (fun x x_1 => Quotient.mk setoid x)
                (_ :
                  ∀ {x y : PGame},
                    Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                0) }
      (Quot.mk Setoid.r { val := val✝¹, property := property✝¹ } +
        Quot.mk Setoid.r { val := val✝, property := property✝ }) =
    ZeroHom.toFun
        {
          toFun :=
            lift (fun x x_1 => Quotient.mk setoid x)
              (_ :
                ∀ {x y : PGame},
                  Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
          map_zero' :=
            (_ :
              lift (fun x x_1 => Quotient.mk setoid x)
                  (_ :
                    ∀ {x y : PGame},
                      Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                  0 =
                lift (fun x x_1 => Quotient.mk setoid x)
                  (_ :
                    ∀ {x y : PGame},
                      Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                  0) }
        (Quot.mk Setoid.r { val := val✝¹, property := property✝¹ }) +
      ZeroHom.toFun
        {
          toFun :=
            lift (fun x x_1 => Quotient.mk setoid x)
              (_ :
                ∀ {x y : PGame},
                  Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
          map_zero' :=
            (_ :
              lift (fun x x_1 => Quotient.mk setoid x)
                  (_ :
                    ∀ {x y : PGame},
                      Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                  0 =
                lift (fun x x_1 => Quotient.mk setoid x)
                  (_ :
                    ∀ {x y : PGame},
                      Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                  0) }
        (Quot.mk Setoid.r { val := val✝, property := property✝ })
[PROOFSTEP]
rfl
[GOAL]
⊢ Monotone
    (↑{
          toZeroHom :=
            {
              toFun :=
                lift (fun x x_1 => Quotient.mk setoid x)
                  (_ :
                    ∀ {x y : PGame},
                      Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
              map_zero' :=
                (_ :
                  lift (fun x x_1 => Quotient.mk setoid x)
                      (_ :
                        ∀ {x y : PGame},
                          Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                      0 =
                    lift (fun x x_1 => Quotient.mk setoid x)
                      (_ :
                        ∀ {x y : PGame},
                          Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                      0) },
          map_add' :=
            (_ :
              ∀ (x y : Surreal),
                ZeroHom.toFun
                    {
                      toFun :=
                        lift (fun x x_1 => Quotient.mk setoid x)
                          (_ :
                            ∀ {x y : PGame},
                              Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
                      map_zero' :=
                        (_ :
                          lift (fun x x_1 => Quotient.mk setoid x)
                              (_ :
                                ∀ {x y : PGame},
                                  Numeric x →
                                    Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                              0 =
                            lift (fun x x_1 => Quotient.mk setoid x)
                              (_ :
                                ∀ {x y : PGame},
                                  Numeric x →
                                    Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                              0) }
                    (x + y) =
                  ZeroHom.toFun
                      {
                        toFun :=
                          lift (fun x x_1 => Quotient.mk setoid x)
                            (_ :
                              ∀ {x y : PGame},
                                Numeric x →
                                  Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
                        map_zero' :=
                          (_ :
                            lift (fun x x_1 => Quotient.mk setoid x)
                                (_ :
                                  ∀ {x y : PGame},
                                    Numeric x →
                                      Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                0 =
                              lift (fun x x_1 => Quotient.mk setoid x)
                                (_ :
                                  ∀ {x y : PGame},
                                    Numeric x →
                                      Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                0) }
                      x +
                    ZeroHom.toFun
                      {
                        toFun :=
                          lift (fun x x_1 => Quotient.mk setoid x)
                            (_ :
                              ∀ {x y : PGame},
                                Numeric x →
                                  Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
                        map_zero' :=
                          (_ :
                            lift (fun x x_1 => Quotient.mk setoid x)
                                (_ :
                                  ∀ {x y : PGame},
                                    Numeric x →
                                      Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                0 =
                              lift (fun x x_1 => Quotient.mk setoid x)
                                (_ :
                                  ∀ {x y : PGame},
                                    Numeric x →
                                      Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                0) }
                      y) }).toFun
[PROOFSTEP]
rintro ⟨_, _⟩ ⟨_, _⟩
[GOAL]
case mk.mk.mk.mk
a✝ : Surreal
val✝¹ : PGame
property✝¹ : Numeric val✝¹
b✝ : Surreal
val✝ : PGame
property✝ : Numeric val✝
⊢ Quot.mk Setoid.r { val := val✝¹, property := property✝¹ } ≤ Quot.mk Setoid.r { val := val✝, property := property✝ } →
    ZeroHom.toFun
        (↑{
            toZeroHom :=
              {
                toFun :=
                  lift (fun x x_1 => Quotient.mk setoid x)
                    (_ :
                      ∀ {x y : PGame},
                        Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
                map_zero' :=
                  (_ :
                    lift (fun x x_1 => Quotient.mk setoid x)
                        (_ :
                          ∀ {x y : PGame},
                            Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                        0 =
                      lift (fun x x_1 => Quotient.mk setoid x)
                        (_ :
                          ∀ {x y : PGame},
                            Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                        0) },
            map_add' :=
              (_ :
                ∀ (x y : Surreal),
                  ZeroHom.toFun
                      {
                        toFun :=
                          lift (fun x x_1 => Quotient.mk setoid x)
                            (_ :
                              ∀ {x y : PGame},
                                Numeric x →
                                  Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
                        map_zero' :=
                          (_ :
                            lift (fun x x_1 => Quotient.mk setoid x)
                                (_ :
                                  ∀ {x y : PGame},
                                    Numeric x →
                                      Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                0 =
                              lift (fun x x_1 => Quotient.mk setoid x)
                                (_ :
                                  ∀ {x y : PGame},
                                    Numeric x →
                                      Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                0) }
                      (x + y) =
                    ZeroHom.toFun
                        {
                          toFun :=
                            lift (fun x x_1 => Quotient.mk setoid x)
                              (_ :
                                ∀ {x y : PGame},
                                  Numeric x →
                                    Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
                          map_zero' :=
                            (_ :
                              lift (fun x x_1 => Quotient.mk setoid x)
                                  (_ :
                                    ∀ {x y : PGame},
                                      Numeric x →
                                        Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                  0 =
                                lift (fun x x_1 => Quotient.mk setoid x)
                                  (_ :
                                    ∀ {x y : PGame},
                                      Numeric x →
                                        Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                  0) }
                        x +
                      ZeroHom.toFun
                        {
                          toFun :=
                            lift (fun x x_1 => Quotient.mk setoid x)
                              (_ :
                                ∀ {x y : PGame},
                                  Numeric x →
                                    Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
                          map_zero' :=
                            (_ :
                              lift (fun x x_1 => Quotient.mk setoid x)
                                  (_ :
                                    ∀ {x y : PGame},
                                      Numeric x →
                                        Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                  0 =
                                lift (fun x x_1 => Quotient.mk setoid x)
                                  (_ :
                                    ∀ {x y : PGame},
                                      Numeric x →
                                        Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                  0) }
                        y) })
        (Quot.mk Setoid.r { val := val✝¹, property := property✝¹ }) ≤
      ZeroHom.toFun
        (↑{
            toZeroHom :=
              {
                toFun :=
                  lift (fun x x_1 => Quotient.mk setoid x)
                    (_ :
                      ∀ {x y : PGame},
                        Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
                map_zero' :=
                  (_ :
                    lift (fun x x_1 => Quotient.mk setoid x)
                        (_ :
                          ∀ {x y : PGame},
                            Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                        0 =
                      lift (fun x x_1 => Quotient.mk setoid x)
                        (_ :
                          ∀ {x y : PGame},
                            Numeric x → Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                        0) },
            map_add' :=
              (_ :
                ∀ (x y : Surreal),
                  ZeroHom.toFun
                      {
                        toFun :=
                          lift (fun x x_1 => Quotient.mk setoid x)
                            (_ :
                              ∀ {x y : PGame},
                                Numeric x →
                                  Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
                        map_zero' :=
                          (_ :
                            lift (fun x x_1 => Quotient.mk setoid x)
                                (_ :
                                  ∀ {x y : PGame},
                                    Numeric x →
                                      Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                0 =
                              lift (fun x x_1 => Quotient.mk setoid x)
                                (_ :
                                  ∀ {x y : PGame},
                                    Numeric x →
                                      Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                0) }
                      (x + y) =
                    ZeroHom.toFun
                        {
                          toFun :=
                            lift (fun x x_1 => Quotient.mk setoid x)
                              (_ :
                                ∀ {x y : PGame},
                                  Numeric x →
                                    Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
                          map_zero' :=
                            (_ :
                              lift (fun x x_1 => Quotient.mk setoid x)
                                  (_ :
                                    ∀ {x y : PGame},
                                      Numeric x →
                                        Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                  0 =
                                lift (fun x x_1 => Quotient.mk setoid x)
                                  (_ :
                                    ∀ {x y : PGame},
                                      Numeric x →
                                        Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                  0) }
                        x +
                      ZeroHom.toFun
                        {
                          toFun :=
                            lift (fun x x_1 => Quotient.mk setoid x)
                              (_ :
                                ∀ {x y : PGame},
                                  Numeric x →
                                    Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y),
                          map_zero' :=
                            (_ :
                              lift (fun x x_1 => Quotient.mk setoid x)
                                  (_ :
                                    ∀ {x y : PGame},
                                      Numeric x →
                                        Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                  0 =
                                lift (fun x x_1 => Quotient.mk setoid x)
                                  (_ :
                                    ∀ {x y : PGame},
                                      Numeric x →
                                        Numeric y → PGame.Equiv x y → Quot.mk PGame.Equiv x = Quot.mk PGame.Equiv y)
                                  0) }
                        y) })
        (Quot.mk Setoid.r { val := val✝, property := property✝ })
[PROOFSTEP]
exact id
[GOAL]
a b : Ordinal.{?u.73448}
h :
  (fun o => Surreal.mk (toPGame o) (_ : Numeric (toPGame o))) a =
    (fun o => Surreal.mk (toPGame o) (_ : Numeric (toPGame o))) b
⊢ toPGame a ≈ toPGame b
[PROOFSTEP]
apply Quotient.exact h