-- Mathlib/SetTheory/Game/PGame.lean
theorem add_le_add_right' : ∀ {x y z : PGame}, x ≤ y → x + z ≤ y + z
  | mk xl xr xL xR, mk yl yr yL yR, mk zl zr zL zR => fun h => by
    refine le_def.2 ⟨fun i => ?_, fun i => ?_⟩ <;> obtain i | i := i
    · rw [le_def] at h
      obtain ⟨h_left, h_right⟩ := h
      rcases h_left i with (⟨i', ih⟩ | ⟨j, jh⟩)
      · exact Or.inl ⟨toLeftMovesAdd (Sum.inl i'), add_le_add_right' ih⟩
      · refine Or.inr ⟨toRightMovesAdd (Sum.inl j), ?_⟩
        convert add_le_add_right' jh
        apply add_moveRight_inl
    · exact Or.inl ⟨@toLeftMovesAdd _ ⟨_, _, _, _⟩ (Sum.inr i), add_le_add_right' h⟩
    · rw [le_def] at h
      rcases h.right i with (⟨i, ih⟩ | ⟨j', jh⟩)
      · refine Or.inl ⟨toLeftMovesAdd (Sum.inl i), ?_⟩
        convert add_le_add_right' ih
        apply add_moveLeft_inl
      · exact Or.inr ⟨toRightMovesAdd (Sum.inl j'), add_le_add_right' jh⟩
    · exact
        Or.inr ⟨@toRightMovesAdd _ ⟨_, _, _, _⟩ (Sum.inr i), add_le_add_right' h⟩
termination_by x y z => (x, y, z)

Proof state:
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', (mk xl xr xL xR + mk zl zr zL zR).moveLeft (Sum.inr i) ≤ (mk yl yr yL yR + mk zl zr zL zR).moveLeft i') ∨
    ∃ j, ((mk xl xr xL xR + mk zl zr zL zR).moveLeft (Sum.inr i)).moveRight j ≤ mk yl yr yL yR + mk zl zr zL zR

Tactic:
exact Or.inl ⟨@toLeftMovesAdd _ ⟨_, _, _, _⟩ (Sum.inr i), add_le_add_right' h⟩

Result:
no goals

Proof state:
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 : (mk xl xr xL xR).LeftMoves),
      (∃ i', (mk xl xr xL xR).moveLeft i ≤ (mk yl yr yL yR).moveLeft i') ∨
        ∃ j, ((mk xl xr xL xR).moveLeft i).moveRight j ≤ mk yl yr yL yR) ∧
    ∀ (j : (mk yl yr yL yR).RightMoves),
      (∃ i, mk xl xr xL xR ≤ ((mk yl yr yL yR).moveRight j).moveLeft i) ∨
        ∃ j', (mk xl xr xL xR).moveRight j' ≤ (mk yl yr yL yR).moveRight j
i✝ : yr
i : ((mk yl yr yL yR).moveRight i✝).LeftMoves
ih : mk xl xr xL xR ≤ ((mk yl yr yL yR).moveRight i✝).moveLeft i
⊢ (∃ i, mk xl xr xL xR + mk zl zr zL zR ≤ ((mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl i✝)).moveLeft i) ∨
    ∃ j', (mk xl xr xL xR + mk zl zr zL zR).moveRight j' ≤ (mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl i✝)

Tactic:
refine Or.inl ⟨toLeftMovesAdd (Sum.inl i), ?_⟩

Result:
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 : (mk xl xr xL xR).LeftMoves),
      (∃ i', (mk xl xr xL xR).moveLeft i ≤ (mk yl yr yL yR).moveLeft i') ∨
        ∃ j, ((mk xl xr xL xR).moveLeft i).moveRight j ≤ mk yl yr yL yR) ∧
    ∀ (j : (mk yl yr yL yR).RightMoves),
      (∃ i, mk xl xr xL xR ≤ ((mk yl yr yL yR).moveRight j).moveLeft i) ∨
        ∃ j', (mk xl xr xL xR).moveRight j' ≤ (mk yl yr yL yR).moveRight j
i✝ : yr
i : ((mk yl yr yL yR).moveRight i✝).LeftMoves
ih : mk xl xr xL xR ≤ ((mk yl yr yL yR).moveRight i✝).moveLeft i
⊢ mk xl xr xL xR + mk zl zr zL zR ≤
    ((mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl i✝)).moveLeft (toLeftMovesAdd (Sum.inl i))

Proof state:
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 ≤ ((mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl i)).moveLeft i_1) ∨
    ∃ j', (mk xl xr xL xR + mk zl zr zL zR).moveRight j' ≤ (mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl i)

Tactic:
rw [le_def] at h

Result:
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 : (mk xl xr xL xR).LeftMoves),
      (∃ i', (mk xl xr xL xR).moveLeft i ≤ (mk yl yr yL yR).moveLeft i') ∨
        ∃ j, ((mk xl xr xL xR).moveLeft i).moveRight j ≤ mk yl yr yL yR) ∧
    ∀ (j : (mk yl yr yL yR).RightMoves),
      (∃ i, mk xl xr xL xR ≤ ((mk yl yr yL yR).moveRight j).moveLeft i) ∨
        ∃ j', (mk xl xr xL xR).moveRight j' ≤ (mk yl yr yL yR).moveRight j
i : yr
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ ((mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl i)).moveLeft i_1) ∨
    ∃ j', (mk xl xr xL xR + mk zl zr zL zR).moveRight j' ≤ (mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl i)

Proof state:
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 : (mk xl xr xL xR).LeftMoves),
      (∃ i', (mk xl xr xL xR).moveLeft i ≤ (mk yl yr yL yR).moveLeft i') ∨
        ∃ j, ((mk xl xr xL xR).moveLeft i).moveRight j ≤ mk yl yr yL yR) ∧
    ∀ (j : (mk yl yr yL yR).RightMoves),
      (∃ i, mk xl xr xL xR ≤ ((mk yl yr yL yR).moveRight j).moveLeft i) ∨
        ∃ j', (mk xl xr xL xR).moveRight j' ≤ (mk yl yr yL yR).moveRight j
i : yr
j' : (mk xl xr xL xR).RightMoves
jh : (mk xl xr xL xR).moveRight j' ≤ (mk yl yr yL yR).moveRight i
⊢ (∃ i_1, mk xl xr xL xR + mk zl zr zL zR ≤ ((mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl i)).moveLeft i_1) ∨
    ∃ j', (mk xl xr xL xR + mk zl zr zL zR).moveRight j' ≤ (mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl i)

Tactic:
exact Or.inr ⟨toRightMovesAdd (Sum.inl j'), add_le_add_right' jh⟩

Result:
no goals