-- Mathlib/SetTheory/Game/PGame.lean
/-- Adding a gift horse left option does not change the value of `x`. A gift horse left option is
 a game `x'` with `x' ⧏ x`. It is called "gift horse" because it seems like Left has gotten the
 "gift" of a new option, but actually the value of the game did not change. -/
lemma insertLeft_equiv_of_lf {x x' : PGame} (h : x' ⧏ x) : insertLeft x x' ≈ x

Proof state:
x x' : PGame
h : x' ⧏ x
⊢ x.insertLeft x' ≤ x ∧ x ≤ x.insertLeft x'

Tactic:
constructor

Result:
case left
x x' : PGame
h : x' ⧏ x
⊢ x.insertLeft x' ≤ x

case right
x x' : PGame
h : x' ⧏ x
⊢ x ≤ x.insertLeft x'

Proof state:
case left.left.mk.inr
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
val✝ : PUnit.{u_1 + 1}
⊢ (∃ i', Sum.elim xL (fun x => x') (Sum.inr val✝) ≤ xL i') ∨
    ∃ j, (Sum.elim xL (fun x => x') (Sum.inr val✝)).moveRight j ≤ mk xl xr xL xR

Tactic:
simp only [Sum.elim_inr]

Result:
case left.left.mk.inr
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
val✝ : PUnit.{u_1 + 1}
⊢ (∃ i', x' ≤ xL i') ∨ ∃ j, x'.moveRight j ≤ mk xl xr xL xR

Proof state:
x x' : PGame
h : x' ⧏ x
⊢ x.insertLeft x' ≈ x

Tactic:
rw [equiv_def]

Result:
x x' : PGame
h : x' ⧏ x
⊢ x.insertLeft x' ≤ x ∧ x ≤ x.insertLeft x'

Proof state:
case left.left
x x' : PGame
h : x' ⧏ x
⊢ ∀ (i : (x.insertLeft x').LeftMoves),
    (∃ i', (x.insertLeft x').moveLeft i ≤ x.moveLeft i') ∨ ∃ j, ((x.insertLeft x').moveLeft i).moveRight j ≤ x

Tactic:
intro i

Result:
case left.left
x x' : PGame
h : x' ⧏ x
i : (x.insertLeft x').LeftMoves
⊢ (∃ i', (x.insertLeft x').moveLeft i ≤ x.moveLeft i') ∨ ∃ j, ((x.insertLeft x').moveLeft i).moveRight j ≤ x

Proof state:
case left
x x' : PGame
h : x' ⧏ x
⊢ (∀ (i : (x.insertLeft x').LeftMoves),
      (∃ i', (x.insertLeft x').moveLeft i ≤ x.moveLeft i') ∨ ∃ j, ((x.insertLeft x').moveLeft i).moveRight j ≤ x) ∧
    ∀ (j : x.RightMoves),
      (∃ i, x.insertLeft x' ≤ (x.moveRight j).moveLeft i) ∨ ∃ j', (x.insertLeft x').moveRight j' ≤ x.moveRight j

Tactic:
constructor

Result:
case left.left
x x' : PGame
h : x' ⧏ x
⊢ ∀ (i : (x.insertLeft x').LeftMoves),
    (∃ i', (x.insertLeft x').moveLeft i ≤ x.moveLeft i') ∨ ∃ j, ((x.insertLeft x').moveLeft i).moveRight j ≤ x

case left.right
x x' : PGame
h : x' ⧏ x
⊢ ∀ (j : x.RightMoves),
    (∃ i, x.insertLeft x' ≤ (x.moveRight j).moveLeft i) ∨ ∃ j', (x.insertLeft x').moveRight j' ≤ x.moveRight j

Proof state:
case left.left.mk.inr
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : (∃ i, x' ≤ (mk xl xr xL xR).moveLeft i) ∨ ∃ j, x'.moveRight j ≤ mk xl xr xL xR
val✝ : PUnit.{u_1 + 1}
⊢ (∃ i', x' ≤ xL i') ∨ ∃ j, x'.moveRight j ≤ mk xl xr xL xR

Tactic:
simp only [leftMoves_mk, moveLeft_mk] at h

Result:
case left.left.mk.inr
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : (∃ i, x' ≤ xL i) ∨ ∃ j, x'.moveRight j ≤ mk xl xr xL xR
val✝ : PUnit.{u_1 + 1}
⊢ (∃ i', x' ≤ xL i') ∨ ∃ j, x'.moveRight j ≤ mk xl xr xL xR

Proof state:
case left.right.h.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
j : (mk xl xr xL xR).RightMoves
⊢ ∃ j', ((mk xl xr xL xR).insertLeft x').moveRight j' ≤ (mk xl xr xL xR).moveRight j

Tactic:
simp only [insertLeft, rightMoves_mk, moveRight_mk]

Result:
case left.right.h.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
j : (mk xl xr xL xR).RightMoves
⊢ ∃ j', xR j' ≤ xR j

Proof state:
case right
x x' : PGame
h : x' ⧏ x
⊢ x ≤ x.insertLeft x'

Tactic:
apply le_insertLeft

Result:
no goals

Proof state:
case left.left.mk.inr
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : (∃ i, x' ≤ xL i) ∨ ∃ j, x'.moveRight j ≤ mk xl xr xL xR
val✝ : PUnit.{u_1 + 1}
⊢ (∃ i', x' ≤ xL i') ∨ ∃ j, x'.moveRight j ≤ mk xl xr xL xR

Tactic:
exact h

Result:
no goals

Proof state:
case left
x x' : PGame
h : x' ⧏ x
⊢ x.insertLeft x' ≤ x

Tactic:
rw [le_def]

Result:
case left
x x' : PGame
h : x' ⧏ x
⊢ (∀ (i : (x.insertLeft x').LeftMoves),
      (∃ i', (x.insertLeft x').moveLeft i ≤ x.moveLeft i') ∨ ∃ j, ((x.insertLeft x').moveLeft i).moveRight j ≤ x) ∧
    ∀ (j : x.RightMoves),
      (∃ i, x.insertLeft x' ≤ (x.moveRight j).moveLeft i) ∨ ∃ j', (x.insertLeft x').moveRight j' ≤ x.moveRight j

Proof state:
case left.right
x x' : PGame
h : x' ⧏ x
j : x.RightMoves
⊢ (∃ i, x.insertLeft x' ≤ (x.moveRight j).moveLeft i) ∨ ∃ j', (x.insertLeft x').moveRight j' ≤ x.moveRight j

Tactic:
right

Result:
case left.right.h
x x' : PGame
h : x' ⧏ x
j : x.RightMoves
⊢ ∃ j', (x.insertLeft x').moveRight j' ≤ x.moveRight j

Proof state:
case left.left.mk.inl
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
i : xl
⊢ (∃ i', Sum.elim xL (fun x => x') (Sum.inl i) ≤ xL i') ∨
    ∃ j, (Sum.elim xL (fun x => x') (Sum.inl i)).moveRight j ≤ mk xl xr xL xR

Tactic:
simp only [Sum.elim_inl]

Result:
case left.left.mk.inl
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
i : xl
⊢ (∃ i', xL i ≤ xL i') ∨ ∃ j, (xL i).moveRight j ≤ mk xl xr xL xR

Proof state:
case left.left.mk.inl.h
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
i : xl
⊢ ∃ i', xL i ≤ xL i'

Tactic:
use i

Result:
no goals

Proof state:
case left.right.h
x x' : PGame
h : x' ⧏ x
j : x.RightMoves
⊢ ∃ j', (x.insertLeft x').moveRight j' ≤ x.moveRight j

Tactic:
rcases x with ⟨xl, xr, xL, xR⟩

Result:
case left.right.h.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
j : (mk xl xr xL xR).RightMoves
⊢ ∃ j', ((mk xl xr xL xR).insertLeft x').moveRight j' ≤ (mk xl xr xL xR).moveRight j

Proof state:
case left.left.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
i : xl ⊕ PUnit.{u_1 + 1}
⊢ (∃ i', Sum.elim xL (fun x => x') i ≤ xL i') ∨ ∃ j, (Sum.elim xL (fun x => x') i).moveRight j ≤ mk xl xr xL xR

Tactic:
rcases i with i | _

Result:
case left.left.mk.inl
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
i : xl
⊢ (∃ i', Sum.elim xL (fun x => x') (Sum.inl i) ≤ xL i') ∨
    ∃ j, (Sum.elim xL (fun x => x') (Sum.inl i)).moveRight j ≤ mk xl xr xL xR

case left.left.mk.inr
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
val✝ : PUnit.{u_1 + 1}
⊢ (∃ i', Sum.elim xL (fun x => x') (Sum.inr val✝) ≤ xL i') ∨
    ∃ j, (Sum.elim xL (fun x => x') (Sum.inr val✝)).moveRight j ≤ mk xl xr xL xR

Proof state:
case left.left.mk.inl
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
i : xl
⊢ (∃ i', xL i ≤ xL i') ∨ ∃ j, (xL i).moveRight j ≤ mk xl xr xL xR

Tactic:
left

Result:
case left.left.mk.inl.h
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
i : xl
⊢ ∃ i', xL i ≤ xL i'

Proof state:
case left.left.mk.inr
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
val✝ : PUnit.{u_1 + 1}
⊢ (∃ i', x' ≤ xL i') ∨ ∃ j, x'.moveRight j ≤ mk xl xr xL xR

Tactic:
rw [lf_iff_exists_le] at h

Result:
case left.left.mk.inr
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : (∃ i, x' ≤ (mk xl xr xL xR).moveLeft i) ∨ ∃ j, x'.moveRight j ≤ mk xl xr xL xR
val✝ : PUnit.{u_1 + 1}
⊢ (∃ i', x' ≤ xL i') ∨ ∃ j, x'.moveRight j ≤ mk xl xr xL xR

Proof state:
case left.right
x x' : PGame
h : x' ⧏ x
⊢ ∀ (j : x.RightMoves),
    (∃ i, x.insertLeft x' ≤ (x.moveRight j).moveLeft i) ∨ ∃ j', (x.insertLeft x').moveRight j' ≤ x.moveRight j

Tactic:
intro j

Result:
case left.right
x x' : PGame
h : x' ⧏ x
j : x.RightMoves
⊢ (∃ i, x.insertLeft x' ≤ (x.moveRight j).moveLeft i) ∨ ∃ j', (x.insertLeft x').moveRight j' ≤ x.moveRight j

Proof state:
case left.right.h.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : x' ⧏ mk xl xr xL xR
j : (mk xl xr xL xR).RightMoves
⊢ ∃ j', xR j' ≤ xR j

Tactic:
use j

Result:
no goals