-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_nadd (a b : Ordinal) : (a ♯ b).toPGame ≈ a.toPGame + b.toPGame

Proof state:
case refine_1.inr.intro.intro.h
a b : Ordinal.{u_1}
i : (a ♯ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < b
hc' : (↑(toLeftMovesToPGame.symm i)).toPGame ≤ a.toPGame + c.toPGame
⊢ c.toPGame ⧏ b.toPGame

Tactic:
rwa [toPGame_lf_iff]

Result:
no goals

Proof state:
case refine_2.hl
a b : Ordinal.{u_1}
i✝ : (a.toPGame + b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
wf : ↑(toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ ↑(toLeftMovesToPGame.symm i) ♯ b < a ♯ b

Tactic:
exact nadd_lt_nadd_right wf _

Result:
no goals

Proof state:
case refine_2.hr
a b : Ordinal.{u_1}
i✝ : (a.toPGame + b.toPGame).LeftMoves
i : b.toPGame.LeftMoves
wf : ↑(toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ a ♯ ↑(toLeftMovesToPGame.symm i) < a ♯ b

Tactic:
exact nadd_lt_nadd_left wf _

Result:
no goals

Proof state:
case refine_1.inr.intro.intro
a b : Ordinal.{u_1}
i : (a ♯ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < b
hc' : (↑(toLeftMovesToPGame.symm i)).toPGame ≤ a.toPGame + c.toPGame
⊢ a.toPGame + c.toPGame ⧏ a.toPGame + b.toPGame

Tactic:
apply add_lf_add_left

Result:
case refine_1.inr.intro.intro.h
a b : Ordinal.{u_1}
i : (a ♯ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < b
hc' : (↑(toLeftMovesToPGame.symm i)).toPGame ≤ a.toPGame + c.toPGame
⊢ c.toPGame ⧏ b.toPGame

Proof state:
case refine_2.hl
a b : Ordinal.{u_1}
i✝ : (a.toPGame + b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
wf : ↑(toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ (a.toPGame + b.toPGame).moveLeft (toLeftMovesAdd (Sum.inl i)) ⧏ (a ♯ b).toPGame

Tactic:
rw [add_moveLeft_inl]

Result:
case refine_2.hl
a b : Ordinal.{u_1}
i✝ : (a.toPGame + b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
wf : ↑(toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ a.toPGame.moveLeft i + b.toPGame ⧏ (a ♯ b).toPGame

Proof state:
case refine_1.inl.intro.intro.h
a b : Ordinal.{u_1}
i : (a ♯ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
hc' : (↑(toLeftMovesToPGame.symm i)).toPGame ≤ c.toPGame + b.toPGame
⊢ c.toPGame ⧏ a.toPGame

Tactic:
rwa [toPGame_lf_iff]

Result:
no goals

Proof state:
case refine_1.inl.intro.intro
a b : Ordinal.{u_1}
i : (a ♯ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
hc' : (↑(toLeftMovesToPGame.symm i)).toPGame ≤ c.toPGame + b.toPGame
⊢ c.toPGame + b.toPGame ⧏ a.toPGame + b.toPGame

Tactic:
apply add_lf_add_right

Result:
case refine_1.inl.intro.intro.h
a b : Ordinal.{u_1}
i : (a ♯ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
hc' : (↑(toLeftMovesToPGame.symm i)).toPGame ≤ c.toPGame + b.toPGame
⊢ c.toPGame ⧏ a.toPGame

Proof state:
case refine_1
a b : Ordinal.{u_1}
i : (a ♯ b).toPGame.LeftMoves
⊢ (a ♯ b).toPGame.moveLeft i ⧏ a.toPGame + b.toPGame

Tactic:
rw [toPGame_moveLeft']

Result:
case refine_1
a b : Ordinal.{u_1}
i : (a ♯ b).toPGame.LeftMoves
⊢ (↑(toLeftMovesToPGame.symm i)).toPGame ⧏ a.toPGame + b.toPGame

Proof state:
case refine_2
a b : Ordinal.{u_1}
i : (a.toPGame + b.toPGame).LeftMoves
⊢ (a.toPGame + b.toPGame).moveLeft i ⧏ (a ♯ b).toPGame

Tactic:
apply leftMoves_add_cases i <;>
intro i <;>
let wf := toLeftMovesToPGame_symm_lt i <;>
(try rw [add_moveLeft_inl]) <;>
(try rw [add_moveLeft_inr]) <;>
rw [toPGame_moveLeft', ← lf_congr_left (toPGame_nadd _ _), toPGame_lf_iff]

Result:
case refine_2.hl
a b : Ordinal.{u_1}
i✝ : (a.toPGame + b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
wf : ↑(toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ ↑(toLeftMovesToPGame.symm i) ♯ b < a ♯ b

case refine_2.hr
a b : Ordinal.{u_1}
i✝ : (a.toPGame + b.toPGame).LeftMoves
i : b.toPGame.LeftMoves
wf : ↑(toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ a ♯ ↑(toLeftMovesToPGame.symm i) < a ♯ b

Proof state:
case refine_2.hl
a b : Ordinal.{u_1}
i✝ : (a.toPGame + b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
wf : ↑(toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ (a.toPGame + b.toPGame).moveLeft (toLeftMovesAdd (Sum.inl i)) ⧏ (a ♯ b).toPGame

Tactic:
try rw [add_moveLeft_inl]

Result:
case refine_2.hl
a b : Ordinal.{u_1}
i✝ : (a.toPGame + b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
wf : ↑(toLeftMovesToPGame.symm i) < a := toLeftMovesToPGame_symm_lt i
⊢ a.toPGame.moveLeft i + b.toPGame ⧏ (a ♯ b).toPGame

Proof state:
case refine_1
a b : Ordinal.{u_1}
i : (a ♯ b).toPGame.LeftMoves
⊢ (↑(toLeftMovesToPGame.symm i)).toPGame ⧏ a.toPGame + b.toPGame

Tactic:
rcases lt_nadd_iff.1 (toLeftMovesToPGame_symm_lt i) with (⟨c, hc, hc'⟩ | ⟨c, hc, hc'⟩) <;>
rw [← toPGame_le_iff, le_congr_right (toPGame_nadd _ _)] at hc' <;>
apply lf_of_le_of_lf hc'

Result:
case refine_1.inl.intro.intro
a b : Ordinal.{u_1}
i : (a ♯ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
hc' : (↑(toLeftMovesToPGame.symm i)).toPGame ≤ c.toPGame + b.toPGame
⊢ c.toPGame + b.toPGame ⧏ a.toPGame + b.toPGame

case refine_1.inr.intro.intro
a b : Ordinal.{u_1}
i : (a ♯ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < b
hc' : (↑(toLeftMovesToPGame.symm i)).toPGame ≤ a.toPGame + c.toPGame
⊢ a.toPGame + c.toPGame ⧏ a.toPGame + b.toPGame

Proof state:
case refine_2.hr
a b : Ordinal.{u_1}
i✝ : (a.toPGame + b.toPGame).LeftMoves
i : b.toPGame.LeftMoves
wf : ↑(toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ (a.toPGame + b.toPGame).moveLeft (toLeftMovesAdd (Sum.inr i)) ⧏ (a ♯ b).toPGame

Tactic:
try rw [add_moveLeft_inr]

Result:
case refine_2.hr
a b : Ordinal.{u_1}
i✝ : (a.toPGame + b.toPGame).LeftMoves
i : b.toPGame.LeftMoves
wf : ↑(toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ a.toPGame + b.toPGame.moveLeft i ⧏ (a ♯ b).toPGame

Proof state:
case refine_2.hr
a b : Ordinal.{u_1}
i✝ : (a.toPGame + b.toPGame).LeftMoves
i : b.toPGame.LeftMoves
wf : ↑(toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ (a.toPGame + b.toPGame).moveLeft (toLeftMovesAdd (Sum.inr i)) ⧏ (a ♯ b).toPGame

Tactic:
rw [add_moveLeft_inr]

Result:
case refine_2.hr
a b : Ordinal.{u_1}
i✝ : (a.toPGame + b.toPGame).LeftMoves
i : b.toPGame.LeftMoves
wf : ↑(toLeftMovesToPGame.symm i) < b := toLeftMovesToPGame_symm_lt i
⊢ a.toPGame + b.toPGame.moveLeft i ⧏ (a ♯ b).toPGame

Proof state:
a b : Ordinal.{u_1}
⊢ (a ♯ b).toPGame ≈ a.toPGame + b.toPGame

Tactic:
refine ⟨le_of_forall_lf (fun i => ?_) isEmptyElim, le_of_forall_lf (fun i => ?_) isEmptyElim⟩

Result:
case refine_1
a b : Ordinal.{u_1}
i : (a ♯ b).toPGame.LeftMoves
⊢ (a ♯ b).toPGame.moveLeft i ⧏ a.toPGame + b.toPGame

case refine_2
a b : Ordinal.{u_1}
i : (a.toPGame + b.toPGame).LeftMoves
⊢ (a.toPGame + b.toPGame).moveLeft i ⧏ (a ♯ b).toPGame