-- Mathlib/SetTheory/Game/PGame.lean
lemma Identical.add_right {x₁ x₂ y} : x₁ ≡ x₂ → x₁ + y ≡ x₂ + y :=
  match x₁, x₂, y with
  | mk x₁l x₁r x₁L x₁R, mk x₂l x₂r x₂L x₂R, mk yl yr yL yR => by
    intro h
    refine ⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩ <;> rintro (_ | _) <;> try exact ⟨.inr _, h.add_right⟩
    · exact (h.1.1 _).elim (⟨.inl ·, ·.add_right⟩)
    · exact (h.1.2 _).elim (⟨.inl ·, ·.add_right⟩)
    · exact (h.2.1 _).elim (⟨.inl ·, ·.add_right⟩)
    · exact (h.2.2 _).elim (⟨.inl ·, ·.add_right⟩)
  termination_by (x₁, x₂, y)

Proof state:
x₁ x₂ y : PGame
x₁l x₁r : Type u_1
x₁L : x₁l → PGame
x₁R : x₁r → PGame
x₂l x₂r : Type u_1
x₂L : x₂l → PGame
x₂R : x₂r → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
h : mk x₁l x₁r x₁L x₁R ≡ mk x₂l x₂r x₂L x₂R
⊢ mk x₁l x₁r x₁L x₁R + mk yl yr yL yR ≡ mk x₂l x₂r x₂L x₂R + mk yl yr yL yR

Tactic:
refine ⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩ <;> rintro (_ | _) <;> try exact ⟨.inr _, h.add_right⟩

Result:
case refine_1.inl
x₁ x₂ y : PGame
x₁l x₁r : Type u_1
x₁L : x₁l → PGame
x₁R : x₁r → PGame
x₂l x₂r : Type u_1
x₂L : x₂l → PGame
x₂R : x₂r → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
h : mk x₁l x₁r x₁L x₁R ≡ mk x₂l x₂r x₂L x₂R
val✝ : x₁l
⊢ ∃ b,
    (fun i j =>
        (fun t =>
              Sum.rec
                (fun i =>
                  (fun a =>
                      rec (motive := fun x => PGame → PGame)
                        (fun xl xr a a IHxl IHxr y =>
                          rec
                            (fun yl yr yL yR IHyl IHyr =>
                              let_fun y := mk yl yr yL yR;
                              mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                Sum.rec (fun i => IHxr i y) IHyr t)
                            y)
                        (x₁L a))
                    i (mk yl yr yL yR))
                (fun a =>
                  rec
                    (fun yl yr yL yR IHyl IHyr =>
                      let_fun y := mk yl yr yL yR;
                      mk (x₁l ⊕ yl) (x₁r ⊕ yr)
                        (fun t =>
                          Sum.rec
                            (fun i =>
                              (fun a =>
                                  rec (motive := fun x => PGame → PGame)
                                    (fun xl xr a a IHxl IHxr y =>
                                      rec
                                        (fun yl yr yL yR IHyl IHyr =>
                                          let_fun y := mk yl yr yL yR;
                                          mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                            Sum.rec (fun i => IHxr i y) IHyr t)
                                        y)
                                    (x₁L a))
                                i y)
                            IHyl t)
                        fun t =>
                        Sum.rec
                          (fun i =>
                            (fun a =>
                                rec (motive := fun x => PGame → PGame)
                                  (fun xl xr a a IHxl IHxr y =>
                                    rec
                                      (fun yl yr yL yR IHyl IHyr =>
                                        let_fun y := mk yl yr yL yR;
                                        mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                          Sum.rec (fun i => IHxr i y) IHyr t)
                                      y)
                                  (x₁R a))
                              i y)
                          IHyr t)
                    (yL a))
                t)
            i ≡
          (fun t =>
              Sum.rec
                (fun i =>
                  (fun a =>
                      rec (motive := fun x => PGame → PGame)
                        (fun xl xr a a IHxl IHxr y =>
                          rec
                            (fun yl yr yL yR IHyl IHyr =>
                              let_fun y := mk yl yr yL yR;
                              mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                Sum.rec (fun i => IHxr i y) IHyr t)
                            y)
                        (x₂L a))
                    i (mk yl yr yL yR))
                (fun a =>
                  rec
                    (fun yl yr yL yR IHyl IHyr =>
                      let_fun y := mk yl yr yL yR;
                      mk (x₂l ⊕ yl) (x₂r ⊕ yr)
                        (fun t =>
                          Sum.rec
                            (fun i =>
                              (fun a =>
                                  rec (motive := fun x => PGame → PGame)
                                    (fun xl xr a a IHxl IHxr y =>
                                      rec
                                        (fun yl yr yL yR IHyl IHyr =>
                                          let_fun y := mk yl yr yL yR;
                                          mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                            Sum.rec (fun i => IHxr i y) IHyr t)
                                        y)
                                    (x₂L a))
                                i y)
                            IHyl t)
                        fun t =>
                        Sum.rec
                          (fun i =>
                            (fun a =>
                                rec (motive := fun x => PGame → PGame)
                                  (fun xl xr a a IHxl IHxr y =>
                                    rec
                                      (fun yl yr yL yR IHyl IHyr =>
                                        let_fun y := mk yl yr yL yR;
                                        mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                          Sum.rec (fun i => IHxr i y) IHyr t)
                                      y)
                                  (x₂R a))
                              i y)
                          IHyr t)
                    (yL a))
                t)
            j)
      (Sum.inl val✝) b

case refine_2.inl
x₁ x₂ y : PGame
x₁l x₁r : Type u_1
x₁L : x₁l → PGame
x₁R : x₁r → PGame
x₂l x₂r : Type u_1
x₂L : x₂l → PGame
x₂R : x₂r → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
h : mk x₁l x₁r x₁L x₁R ≡ mk x₂l x₂r x₂L x₂R
val✝ : x₂l
⊢ ∃ a,
    (fun i j =>
        (fun t =>
              Sum.rec
                (fun i =>
                  (fun a =>
                      rec (motive := fun x => PGame → PGame)
                        (fun xl xr a a IHxl IHxr y =>
                          rec
                            (fun yl yr yL yR IHyl IHyr =>
                              let_fun y := mk yl yr yL yR;
                              mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                Sum.rec (fun i => IHxr i y) IHyr t)
                            y)
                        (x₁L a))
                    i (mk yl yr yL yR))
                (fun a =>
                  rec
                    (fun yl yr yL yR IHyl IHyr =>
                      let_fun y := mk yl yr yL yR;
                      mk (x₁l ⊕ yl) (x₁r ⊕ yr)
                        (fun t =>
                          Sum.rec
                            (fun i =>
                              (fun a =>
                                  rec (motive := fun x => PGame → PGame)
                                    (fun xl xr a a IHxl IHxr y =>
                                      rec
                                        (fun yl yr yL yR IHyl IHyr =>
                                          let_fun y := mk yl yr yL yR;
                                          mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                            Sum.rec (fun i => IHxr i y) IHyr t)
                                        y)
                                    (x₁L a))
                                i y)
                            IHyl t)
                        fun t =>
                        Sum.rec
                          (fun i =>
                            (fun a =>
                                rec (motive := fun x => PGame → PGame)
                                  (fun xl xr a a IHxl IHxr y =>
                                    rec
                                      (fun yl yr yL yR IHyl IHyr =>
                                        let_fun y := mk yl yr yL yR;
                                        mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                          Sum.rec (fun i => IHxr i y) IHyr t)
                                      y)
                                  (x₁R a))
                              i y)
                          IHyr t)
                    (yL a))
                t)
            i ≡
          (fun t =>
              Sum.rec
                (fun i =>
                  (fun a =>
                      rec (motive := fun x => PGame → PGame)
                        (fun xl xr a a IHxl IHxr y =>
                          rec
                            (fun yl yr yL yR IHyl IHyr =>
                              let_fun y := mk yl yr yL yR;
                              mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                Sum.rec (fun i => IHxr i y) IHyr t)
                            y)
                        (x₂L a))
                    i (mk yl yr yL yR))
                (fun a =>
                  rec
                    (fun yl yr yL yR IHyl IHyr =>
                      let_fun y := mk yl yr yL yR;
                      mk (x₂l ⊕ yl) (x₂r ⊕ yr)
                        (fun t =>
                          Sum.rec
                            (fun i =>
                              (fun a =>
                                  rec (motive := fun x => PGame → PGame)
                                    (fun xl xr a a IHxl IHxr y =>
                                      rec
                                        (fun yl yr yL yR IHyl IHyr =>
                                          let_fun y := mk yl yr yL yR;
                                          mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                            Sum.rec (fun i => IHxr i y) IHyr t)
                                        y)
                                    (x₂L a))
                                i y)
                            IHyl t)
                        fun t =>
                        Sum.rec
                          (fun i =>
                            (fun a =>
                                rec (motive := fun x => PGame → PGame)
                                  (fun xl xr a a IHxl IHxr y =>
                                    rec
                                      (fun yl yr yL yR IHyl IHyr =>
                                        let_fun y := mk yl yr yL yR;
                                        mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                          Sum.rec (fun i => IHxr i y) IHyr t)
                                      y)
                                  (x₂R a))
                              i y)
                          IHyr t)
                    (yL a))
                t)
            j)
      a (Sum.inl val✝)

case refine_3.inl
x₁ x₂ y : PGame
x₁l x₁r : Type u_1
x₁L : x₁l → PGame
x₁R : x₁r → PGame
x₂l x₂r : Type u_1
x₂L : x₂l → PGame
x₂R : x₂r → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
h : mk x₁l x₁r x₁L x₁R ≡ mk x₂l x₂r x₂L x₂R
val✝ : x₁r
⊢ ∃ b,
    (fun i j =>
        (fun t =>
              Sum.rec
                (fun i =>
                  (fun a =>
                      rec (motive := fun x => PGame → PGame)
                        (fun xl xr a a IHxl IHxr y =>
                          rec
                            (fun yl yr yL yR IHyl IHyr =>
                              let_fun y := mk yl yr yL yR;
                              mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                Sum.rec (fun i => IHxr i y) IHyr t)
                            y)
                        (x₁R a))
                    i (mk yl yr yL yR))
                (fun a =>
                  rec
                    (fun yl yr yL yR IHyl IHyr =>
                      let_fun y := mk yl yr yL yR;
                      mk (x₁l ⊕ yl) (x₁r ⊕ yr)
                        (fun t =>
                          Sum.rec
                            (fun i =>
                              (fun a =>
                                  rec (motive := fun x => PGame → PGame)
                                    (fun xl xr a a IHxl IHxr y =>
                                      rec
                                        (fun yl yr yL yR IHyl IHyr =>
                                          let_fun y := mk yl yr yL yR;
                                          mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                            Sum.rec (fun i => IHxr i y) IHyr t)
                                        y)
                                    (x₁L a))
                                i y)
                            IHyl t)
                        fun t =>
                        Sum.rec
                          (fun i =>
                            (fun a =>
                                rec (motive := fun x => PGame → PGame)
                                  (fun xl xr a a IHxl IHxr y =>
                                    rec
                                      (fun yl yr yL yR IHyl IHyr =>
                                        let_fun y := mk yl yr yL yR;
                                        mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                          Sum.rec (fun i => IHxr i y) IHyr t)
                                      y)
                                  (x₁R a))
                              i y)
                          IHyr t)
                    (yR a))
                t)
            i ≡
          (fun t =>
              Sum.rec
                (fun i =>
                  (fun a =>
                      rec (motive := fun x => PGame → PGame)
                        (fun xl xr a a IHxl IHxr y =>
                          rec
                            (fun yl yr yL yR IHyl IHyr =>
                              let_fun y := mk yl yr yL yR;
                              mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                Sum.rec (fun i => IHxr i y) IHyr t)
                            y)
                        (x₂R a))
                    i (mk yl yr yL yR))
                (fun a =>
                  rec
                    (fun yl yr yL yR IHyl IHyr =>
                      let_fun y := mk yl yr yL yR;
                      mk (x₂l ⊕ yl) (x₂r ⊕ yr)
                        (fun t =>
                          Sum.rec
                            (fun i =>
                              (fun a =>
                                  rec (motive := fun x => PGame → PGame)
                                    (fun xl xr a a IHxl IHxr y =>
                                      rec
                                        (fun yl yr yL yR IHyl IHyr =>
                                          let_fun y := mk yl yr yL yR;
                                          mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                            Sum.rec (fun i => IHxr i y) IHyr t)
                                        y)
                                    (x₂L a))
                                i y)
                            IHyl t)
                        fun t =>
                        Sum.rec
                          (fun i =>
                            (fun a =>
                                rec (motive := fun x => PGame → PGame)
                                  (fun xl xr a a IHxl IHxr y =>
                                    rec
                                      (fun yl yr yL yR IHyl IHyr =>
                                        let_fun y := mk yl yr yL yR;
                                        mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                          Sum.rec (fun i => IHxr i y) IHyr t)
                                      y)
                                  (x₂R a))
                              i y)
                          IHyr t)
                    (yR a))
                t)
            j)
      (Sum.inl val✝) b

case refine_4.inl
x₁ x₂ y : PGame
x₁l x₁r : Type u_1
x₁L : x₁l → PGame
x₁R : x₁r → PGame
x₂l x₂r : Type u_1
x₂L : x₂l → PGame
x₂R : x₂r → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
h : mk x₁l x₁r x₁L x₁R ≡ mk x₂l x₂r x₂L x₂R
val✝ : x₂r
⊢ ∃ a,
    (fun i j =>
        (fun t =>
              Sum.rec
                (fun i =>
                  (fun a =>
                      rec (motive := fun x => PGame → PGame)
                        (fun xl xr a a IHxl IHxr y =>
                          rec
                            (fun yl yr yL yR IHyl IHyr =>
                              let_fun y := mk yl yr yL yR;
                              mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                Sum.rec (fun i => IHxr i y) IHyr t)
                            y)
                        (x₁R a))
                    i (mk yl yr yL yR))
                (fun a =>
                  rec
                    (fun yl yr yL yR IHyl IHyr =>
                      let_fun y := mk yl yr yL yR;
                      mk (x₁l ⊕ yl) (x₁r ⊕ yr)
                        (fun t =>
                          Sum.rec
                            (fun i =>
                              (fun a =>
                                  rec (motive := fun x => PGame → PGame)
                                    (fun xl xr a a IHxl IHxr y =>
                                      rec
                                        (fun yl yr yL yR IHyl IHyr =>
                                          let_fun y := mk yl yr yL yR;
                                          mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                            Sum.rec (fun i => IHxr i y) IHyr t)
                                        y)
                                    (x₁L a))
                                i y)
                            IHyl t)
                        fun t =>
                        Sum.rec
                          (fun i =>
                            (fun a =>
                                rec (motive := fun x => PGame → PGame)
                                  (fun xl xr a a IHxl IHxr y =>
                                    rec
                                      (fun yl yr yL yR IHyl IHyr =>
                                        let_fun y := mk yl yr yL yR;
                                        mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                          Sum.rec (fun i => IHxr i y) IHyr t)
                                      y)
                                  (x₁R a))
                              i y)
                          IHyr t)
                    (yR a))
                t)
            i ≡
          (fun t =>
              Sum.rec
                (fun i =>
                  (fun a =>
                      rec (motive := fun x => PGame → PGame)
                        (fun xl xr a a IHxl IHxr y =>
                          rec
                            (fun yl yr yL yR IHyl IHyr =>
                              let_fun y := mk yl yr yL yR;
                              mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                Sum.rec (fun i => IHxr i y) IHyr t)
                            y)
                        (x₂R a))
                    i (mk yl yr yL yR))
                (fun a =>
                  rec
                    (fun yl yr yL yR IHyl IHyr =>
                      let_fun y := mk yl yr yL yR;
                      mk (x₂l ⊕ yl) (x₂r ⊕ yr)
                        (fun t =>
                          Sum.rec
                            (fun i =>
                              (fun a =>
                                  rec (motive := fun x => PGame → PGame)
                                    (fun xl xr a a IHxl IHxr y =>
                                      rec
                                        (fun yl yr yL yR IHyl IHyr =>
                                          let_fun y := mk yl yr yL yR;
                                          mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                            Sum.rec (fun i => IHxr i y) IHyr t)
                                        y)
                                    (x₂L a))
                                i y)
                            IHyl t)
                        fun t =>
                        Sum.rec
                          (fun i =>
                            (fun a =>
                                rec (motive := fun x => PGame → PGame)
                                  (fun xl xr a a IHxl IHxr y =>
                                    rec
                                      (fun yl yr yL yR IHyl IHyr =>
                                        let_fun y := mk yl yr yL yR;
                                        mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                          Sum.rec (fun i => IHxr i y) IHyr t)
                                      y)
                                  (x₂R a))
                              i y)
                          IHyr t)
                    (yR a))
                t)
            j)
      a (Sum.inl val✝)