case refine'_1.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
i : xl
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR

case refine'_1.inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
i : zl
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inr i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inr i)) j ≤ mk yl yr yL yR + mk zl zr zL zR

case refine'_2.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
i : yr
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)) i_1) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)

case refine'_2.inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
i : zr
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inr i)) i_1) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inr i)
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
⊢ mk xl xr xL xR + mk zl zr zL zR ≤ mk yl yr yL yR + mk zl zr zL zR
refine' le_def.2 ⟨fun i => _, fun i => _⟩ <;> cases' i with i i
case refine'_1.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i : xl
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
case refine'_1.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
i : xl
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
rw [le_def] at h
case refine'_1.inl.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
case refine'_1.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i : xl
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
cases' h with h_left h_right
case refine'_1.inl.intro.inl.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i' : LeftMoves (mk yl yr yL yR)
ih : moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i'
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR

case refine'_1.inl.intro.inr.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
j : RightMoves (moveLeft (mk xl xr xL xR) i)
jh : moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
case refine'_1.inl.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
rcases h_left i with (⟨i', ih⟩ | ⟨j, jh⟩)
no goals
case refine'_1.inl.intro.inl.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i' : LeftMoves (mk yl yr yL yR)
ih : moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i'
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
exact Or.inl ⟨toLeftMovesAdd (Sum.inl i'), add_le_add_right' ih⟩
case refine'_1.inl.intro.inr.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
j : RightMoves (moveLeft (mk xl xr xL xR) i)
jh : moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
⊢ moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) (↑toRightMovesAdd (Sum.inl j)) ≤
    mk yl yr yL yR + mk zl zr zL zR
case refine'_1.inl.intro.inr.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
j : RightMoves (moveLeft (mk xl xr xL xR) i)
jh : moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
refine' Or.inr ⟨toRightMovesAdd (Sum.inl j), _⟩
case h.e'_3
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
j : RightMoves (moveLeft (mk xl xr xL xR) i)
jh : moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
⊢ moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) (↑toRightMovesAdd (Sum.inl j)) =
    moveRight (moveLeft (mk xl xr xL xR) i) j + mk zl zr zL zR
case refine'_1.inl.intro.inr.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
j : RightMoves (moveLeft (mk xl xr xL xR) i)
jh : moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
⊢ moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) (↑toRightMovesAdd (Sum.inl j)) ≤
    mk yl yr yL yR + mk zl zr zL zR
convert add_le_add_right' jh
no goals
case h.e'_3
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
i : xl
h_left :
  ∀ (i : LeftMoves (mk xl xr xL xR)),
    (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
      ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
h_right :
  ∀ (j : RightMoves (mk yl yr yL yR)),
    (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
      ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
j : RightMoves (moveLeft (mk xl xr xL xR) i)
jh : moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR
⊢ moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inl i)) (↑toRightMovesAdd (Sum.inl j)) =
    moveRight (moveLeft (mk xl xr xL xR) i) j + mk zl zr zL zR
apply add_moveRight_inl
no goals
case refine'_1.inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
i : zl
⊢ (∃ i', moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inr i) ≤ moveLeft (mk yl yr yL yR + mk zl zr zL zR) i') ∨
    ∃ j, moveRight (moveLeft (mk xl xr xL xR + mk zl zr zL zR) (Sum.inr i)) j ≤ mk yl yr yL yR + mk zl zr zL zR
exact Or.inl ⟨@toLeftMovesAdd _ ⟨_, _, _, _⟩ (Sum.inr i), add_le_add_right' h⟩
case refine'_2.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i : yr
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)) i_1) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)
case refine'_2.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
i : yr
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)) i_1) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)
rw [le_def] at h
case refine'_2.inl.inl.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i✝ : yr
i : LeftMoves (moveRight (mk yl yr yL yR) i✝)
ih : mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) i✝) i
⊢ (∃ i, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i✝)) i) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i✝)

case refine'_2.inl.inr.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i : yr
j' : RightMoves (mk xl xr xL xR)
jh : moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) i
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)) i_1) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)
case refine'_2.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i : yr
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)) i_1) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)
rcases h.right i with (⟨i, ih⟩ | ⟨j', jh⟩)
case refine'_2.inl.inl.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i✝ : yr
i : LeftMoves (moveRight (mk yl yr yL yR) i✝)
ih : mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) i✝) i
⊢ mk xl xr xL xR + mk zl zr zL zR ≤
    moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i✝)) (↑toLeftMovesAdd (Sum.inl i))
case refine'_2.inl.inl.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i✝ : yr
i : LeftMoves (moveRight (mk yl yr yL yR) i✝)
ih : mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) i✝) i
⊢ (∃ i, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i✝)) i) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i✝)
refine' Or.inl ⟨toLeftMovesAdd (Sum.inl i), _⟩
case h.e'_4
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i✝ : yr
i : LeftMoves (moveRight (mk yl yr yL yR) i✝)
ih : mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) i✝) i
⊢ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i✝)) (↑toLeftMovesAdd (Sum.inl i)) =
    moveLeft (moveRight (mk yl yr yL yR) i✝) i + mk zl zr zL zR
case refine'_2.inl.inl.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i✝ : yr
i : LeftMoves (moveRight (mk yl yr yL yR) i✝)
ih : mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) i✝) i
⊢ mk xl xr xL xR + mk zl zr zL zR ≤
    moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i✝)) (↑toLeftMovesAdd (Sum.inl i))
convert add_le_add_right' ih
no goals
case h.e'_4
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i✝ : yr
i : LeftMoves (moveRight (mk yl yr yL yR) i✝)
ih : mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) i✝) i
⊢ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i✝)) (↑toLeftMovesAdd (Sum.inl i)) =
    moveLeft (moveRight (mk yl yr yL yR) i✝) i + mk zl zr zL zR
apply add_moveLeft_inl
no goals
case refine'_2.inl.inr.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h :
  (∀ (i : LeftMoves (mk xl xr xL xR)),
      (∃ i', moveLeft (mk xl xr xL xR) i ≤ moveLeft (mk yl yr yL yR) i') ∨
        ∃ j, moveRight (moveLeft (mk xl xr xL xR) i) j ≤ mk yl yr yL yR) ∧
    ∀ (j : RightMoves (mk yl yr yL yR)),
      (∃ i, mk xl xr xL xR ≤ moveLeft (moveRight (mk yl yr yL yR) j) i) ∨
        ∃ j', moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) j
i : yr
j' : RightMoves (mk xl xr xL xR)
jh : moveRight (mk xl xr xL xR) j' ≤ moveRight (mk yl yr yL yR) i
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)) i_1) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inl i)
exact Or.inr ⟨toRightMovesAdd (Sum.inl j'), add_le_add_right' jh⟩
no goals
case refine'_2.inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
h : mk xl xr xL xR ≤ mk yl yr yL yR
i : zr
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ moveLeft (moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inr i)) i_1) ∨
    ∃ j', moveRight (mk xl xr xL xR + mk zl zr zL zR) j' ≤ moveRight (mk yl yr yL yR + mk zl zr zL zR) (Sum.inr i)
exact
  Or.inr ⟨@toRightMovesAdd _ ⟨_, _, _, _⟩ (Sum.inr i), add_le_add_right' h⟩