[GOAL]
o : Ordinal.{u_1}
⊢ let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1);
  toPGame o = mk (Quotient.out o).α PEmpty (fun x => toPGame (typein (fun x x_1 => x < x_1) x)) PEmpty.elim
[PROOFSTEP]
rw [toPGame]
[GOAL]
o : Ordinal.{u_1}
⊢ LeftMoves (toPGame o) = (Quotient.out o).α
[PROOFSTEP]
rw [toPGame, LeftMoves]
[GOAL]
o : Ordinal.{u_1}
⊢ RightMoves (toPGame o) = PEmpty
[PROOFSTEP]
rw [toPGame, RightMoves]
[GOAL]
⊢ IsEmpty (LeftMoves (toPGame 0))
[PROOFSTEP]
rw [toPGame_leftMoves]
[GOAL]
⊢ IsEmpty (Quotient.out 0).α
[PROOFSTEP]
infer_instance
[GOAL]
o : Ordinal.{?u.8904}
⊢ IsEmpty (RightMoves (toPGame o))
[PROOFSTEP]
rw [toPGame_rightMoves]
[GOAL]
o : Ordinal.{?u.8904}
⊢ IsEmpty PEmpty
[PROOFSTEP]
infer_instance
[GOAL]
o : Ordinal.{u_1}
⊢ let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1);
  HEq (moveLeft (toPGame o)) fun x => toPGame (typein (fun x x_1 => x < x_1) x)
[PROOFSTEP]
rw [toPGame]
[GOAL]
o : Ordinal.{u_1}
⊢ let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1);
  HEq
    (moveLeft
      ((fun this =>
          mk (Quotient.out o).α PEmpty
            (fun x =>
              let_fun this_1 := (_ : typein (fun x x_1 => x < x_1) x < o);
              toPGame (typein (fun x x_1 => x < x_1) x))
            PEmpty.elim)
        (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1)))
    fun x => toPGame (typein (fun x x_1 => x < x_1) x)
[PROOFSTEP]
rfl
[GOAL]
o : Ordinal.{u_1}
i : ↑(Set.Iio o)
⊢ moveLeft (toPGame o) (↑toLeftMovesToPGame i) = toPGame ↑i
[PROOFSTEP]
simp
[GOAL]
i : LeftMoves (toPGame 1)
⊢ ↑toLeftMovesToPGame.symm i = { val := 0, property := (_ : 0 ∈ Set.Iio 1) }
[PROOFSTEP]
simp
[GOAL]
x : LeftMoves (toPGame 1)
⊢ moveLeft (toPGame 1) x = toPGame 0
[PROOFSTEP]
simp
[GOAL]
i : LeftMoves (toPGame 1)
⊢ moveLeft (toPGame 1) i ≡r moveLeft 1 (↑(Equiv.equivOfUnique (LeftMoves (toPGame 1)) (LeftMoves 1)) i)
[PROOFSTEP]
simpa using zeroToPgameRelabelling
[GOAL]
a b : Ordinal.{u_1}
h : a < b
⊢ toPGame a ⧏ toPGame b
[PROOFSTEP]
convert moveLeft_lf (toLeftMovesToPGame ⟨a, h⟩)
[GOAL]
case h.e'_1
a b : Ordinal.{u_1}
h : a < b
⊢ toPGame a = moveLeft (toPGame b) (↑toLeftMovesToPGame { val := a, property := h })
[PROOFSTEP]
rw [toPGame_moveLeft]
[GOAL]
a b : Ordinal.{u_1}
h : a ≤ b
⊢ toPGame a ≤ toPGame b
[PROOFSTEP]
refine' le_iff_forall_lf.2 ⟨fun i => _, isEmptyElim⟩
[GOAL]
a b : Ordinal.{u_1}
h : a ≤ b
i : LeftMoves (toPGame a)
⊢ moveLeft (toPGame a) i ⧏ toPGame b
[PROOFSTEP]
rw [toPGame_moveLeft']
[GOAL]
a b : Ordinal.{u_1}
h : a ≤ b
i : LeftMoves (toPGame a)
⊢ toPGame ↑(↑toLeftMovesToPGame.symm i) ⧏ toPGame b
[PROOFSTEP]
exact toPGame_lf ((toLeftMovesToPGame_symm_lt i).trans_le h)
[GOAL]
a b : Ordinal.{u_1}
⊢ toPGame a ⧏ toPGame b → a < b
[PROOFSTEP]
contrapose
[GOAL]
a b : Ordinal.{u_1}
⊢ ¬a < b → ¬toPGame a ⧏ toPGame b
[PROOFSTEP]
rw [not_lt, not_lf]
[GOAL]
a b : Ordinal.{u_1}
⊢ b ≤ a → toPGame b ≤ toPGame a
[PROOFSTEP]
exact toPGame_le
[GOAL]
a b : Ordinal.{u_1}
⊢ toPGame a ≤ toPGame b → a ≤ b
[PROOFSTEP]
contrapose
[GOAL]
a b : Ordinal.{u_1}
⊢ ¬a ≤ b → ¬toPGame a ≤ toPGame b
[PROOFSTEP]
rw [not_le, PGame.not_le]
[GOAL]
a b : Ordinal.{u_1}
⊢ b < a → toPGame b ⧏ toPGame a
[PROOFSTEP]
exact toPGame_lf
[GOAL]
a b : Ordinal.{u_1}
⊢ toPGame a < toPGame b → a < b
[PROOFSTEP]
contrapose
[GOAL]
a b : Ordinal.{u_1}
⊢ ¬a < b → ¬toPGame a < toPGame b
[PROOFSTEP]
rw [not_lt]
[GOAL]
a b : Ordinal.{u_1}
⊢ b ≤ a → ¬toPGame a < toPGame b
[PROOFSTEP]
exact fun h => not_lt_of_le (toPGame_le h)
[GOAL]
a b : Ordinal.{u_1}
⊢ toPGame a ≈ toPGame b ↔ a = b
[PROOFSTEP]
change _ ≤ _ ∧ _ ≤ _ ↔ _
[GOAL]
a b : Ordinal.{u_1}
⊢ toPGame a ≤ toPGame b ∧ toPGame b ≤ toPGame a ↔ a = b
[PROOFSTEP]
rw [le_antisymm_iff, toPGame_le_iff, toPGame_le_iff]
[GOAL]
a b : Ordinal.{u}
⊢ toPGame a + toPGame b ≈ toPGame (a ♯ b)
[PROOFSTEP]
refine' ⟨le_of_forall_lf (fun i => _) isEmptyElim, le_of_forall_lf (fun i => _) isEmptyElim⟩
[GOAL]
case refine'_1
a b : Ordinal.{u}
i : LeftMoves (toPGame a + toPGame b)
⊢ moveLeft (toPGame a + toPGame b) i ⧏ toPGame (a ♯ b)
[PROOFSTEP]
apply leftMoves_add_cases i
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i : LeftMoves (toPGame a + toPGame b)
⊢ ∀ (i : LeftMoves (toPGame a)), moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inl i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
intro i
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i : LeftMoves (toPGame a + toPGame b)
⊢ ∀ (i : LeftMoves (toPGame b)), moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inr i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
intro i
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame a)
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inl i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
let wf := toLeftMovesToPGame_symm_lt i
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame b)
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inr i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
let wf := toLeftMovesToPGame_symm_lt i
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame a)
wf : ↑(↑toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inl i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
try rw [add_moveLeft_inl]
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame a)
wf : ↑(↑toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inl i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
rw [add_moveLeft_inl]
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame b)
wf : ↑(↑toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inr i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
try rw [add_moveLeft_inl]
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame b)
wf : ↑(↑toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inr i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
rw [add_moveLeft_inl]
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame a)
wf : ↑(↑toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a) i + toPGame b ⧏ toPGame (a ♯ b)
[PROOFSTEP]
try rw [add_moveLeft_inr]
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame a)
wf : ↑(↑toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a) i + toPGame b ⧏ toPGame (a ♯ b)
[PROOFSTEP]
rw [add_moveLeft_inr]
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame b)
wf : ↑(↑toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inr i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
try rw [add_moveLeft_inr]
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame b)
wf : ↑(↑toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a + toPGame b) (↑toLeftMovesAdd (Sum.inr i)) ⧏ toPGame (a ♯ b)
[PROOFSTEP]
rw [add_moveLeft_inr]
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame a)
wf : ↑(↑toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ moveLeft (toPGame a) i + toPGame b ⧏ toPGame (a ♯ b)
[PROOFSTEP]
rw [toPGame_moveLeft', lf_congr_left (toPGame_add _ _), toPGame_lf_iff]
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame b)
wf : ↑(↑toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ toPGame a + moveLeft (toPGame b) i ⧏ toPGame (a ♯ b)
[PROOFSTEP]
rw [toPGame_moveLeft', lf_congr_left (toPGame_add _ _), toPGame_lf_iff]
[GOAL]
case refine'_1.hl
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame a)
wf : ↑(↑toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ ↑(↑toLeftMovesToPGame.symm i) ♯ b < a ♯ b
[PROOFSTEP]
exact nadd_lt_nadd_right wf _
[GOAL]
case refine'_1.hr
a b : Ordinal.{u}
i✝ : LeftMoves (toPGame a + toPGame b)
i : LeftMoves (toPGame b)
wf : ↑(↑toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ a ♯ ↑(↑toLeftMovesToPGame.symm i) < a ♯ b
[PROOFSTEP]
exact nadd_lt_nadd_left wf _
[GOAL]
case refine'_2
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
⊢ moveLeft (toPGame (a ♯ b)) i ⧏ toPGame a + toPGame b
[PROOFSTEP]
rw [toPGame_moveLeft']
[GOAL]
case refine'_2
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
⊢ toPGame ↑(↑toLeftMovesToPGame.symm i) ⧏ toPGame a + toPGame b
[PROOFSTEP]
rcases lt_nadd_iff.1 (toLeftMovesToPGame_symm_lt i) with (⟨c, hc, hc'⟩ | ⟨c, hc, hc'⟩)
[GOAL]
case refine'_2.inl.intro.intro
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < a
hc' : ↑(↑toLeftMovesToPGame.symm i) ≤ c ♯ b
⊢ toPGame ↑(↑toLeftMovesToPGame.symm i) ⧏ toPGame a + toPGame b
[PROOFSTEP]
rw [← toPGame_le_iff, ← le_congr_right (toPGame_add _ _)] at hc' 
[GOAL]
case refine'_2.inr.intro.intro
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < b
hc' : ↑(↑toLeftMovesToPGame.symm i) ≤ a ♯ c
⊢ toPGame ↑(↑toLeftMovesToPGame.symm i) ⧏ toPGame a + toPGame b
[PROOFSTEP]
rw [← toPGame_le_iff, ← le_congr_right (toPGame_add _ _)] at hc' 
[GOAL]
case refine'_2.inl.intro.intro
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < a
hc' : toPGame ↑(↑toLeftMovesToPGame.symm i) ≤ toPGame c + toPGame b
⊢ toPGame ↑(↑toLeftMovesToPGame.symm i) ⧏ toPGame a + toPGame b
[PROOFSTEP]
apply lf_of_le_of_lf hc'
[GOAL]
case refine'_2.inr.intro.intro
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < b
hc' : toPGame ↑(↑toLeftMovesToPGame.symm i) ≤ toPGame a + toPGame c
⊢ toPGame ↑(↑toLeftMovesToPGame.symm i) ⧏ toPGame a + toPGame b
[PROOFSTEP]
apply lf_of_le_of_lf hc'
[GOAL]
case refine'_2.inl.intro.intro
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < a
hc' : toPGame ↑(↑toLeftMovesToPGame.symm i) ≤ toPGame c + toPGame b
⊢ toPGame c + toPGame b ⧏ toPGame a + toPGame b
[PROOFSTEP]
apply add_lf_add_right
[GOAL]
case refine'_2.inl.intro.intro.h
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < a
hc' : toPGame ↑(↑toLeftMovesToPGame.symm i) ≤ toPGame c + toPGame b
⊢ toPGame c ⧏ toPGame a
[PROOFSTEP]
rwa [toPGame_lf_iff]
[GOAL]
case refine'_2.inr.intro.intro
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < b
hc' : toPGame ↑(↑toLeftMovesToPGame.symm i) ≤ toPGame a + toPGame c
⊢ toPGame a + toPGame c ⧏ toPGame a + toPGame b
[PROOFSTEP]
apply add_lf_add_left
[GOAL]
case refine'_2.inr.intro.intro.h
a b : Ordinal.{u}
i : LeftMoves (toPGame (a ♯ b))
c : Ordinal.{u}
hc : c < b
hc' : toPGame ↑(↑toLeftMovesToPGame.symm i) ≤ toPGame a + toPGame c
⊢ toPGame c ⧏ toPGame b
[PROOFSTEP]
rwa [toPGame_lf_iff]
