-- 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:
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

Tactic:
refine le_def.2 ⟨fun i => ?_, fun i => ?_⟩ <;> obtain i | i := i

Result:
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', (mk xl xr xL xR + mk zl zr zL zR).moveLeft (Sum.inl 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.inl i)).moveRight 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', (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

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)

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 ≤ ((mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inr 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.inr i)

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
⊢ 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))

Tactic:
convert add_le_add_right' ih

Result:
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 : (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 yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl i✝)).moveLeft (toLeftMovesAdd (Sum.inl i)) =
    ((mk yl yr yL yR).moveRight i✝).moveLeft i + mk zl zr zL zR

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

Tactic:
convert add_le_add_right' jh

Result:
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 : (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
h_right :
  ∀ (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
j : ((mk xl xr xL xR).moveLeft i).RightMoves
jh : ((mk xl xr xL xR).moveLeft i).moveRight j ≤ mk yl yr yL yR
⊢ ((mk xl xr xL xR + mk zl zr zL zR).moveLeft (Sum.inl i)).moveRight (toRightMovesAdd (Sum.inl j)) =
    ((mk xl xr xL xR).moveLeft i).moveRight j + mk zl zr zL zR

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

Tactic:
rw [le_def] at h

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