-- Mathlib/SetTheory/Surreal/Basic.lean
theorem add : ∀ {x y : PGame} (_ : Numeric x) (_ : Numeric y), Numeric (x + y)
  | ⟨xl, xr, xL, xR⟩, ⟨yl, yr, yL, yR⟩, ox, oy =>
    ⟨by
      rintro (ix | iy) (jx | jy)
      · exact add_lt_add_right (ox.1 ix jx) _
      · exact (add_lf_add_of_lf_of_le (lf_mk _ _ ix) (oy.le_moveRight jy)).lt
          ((ox.moveLeft ix).add oy) (ox.add (oy.moveRight jy))
      · exact (add_lf_add_of_lf_of_le (mk_lf _ _ jx) (oy.moveLeft_le iy)).lt
          (ox.add (oy.moveLeft iy)) ((ox.moveRight jx).add oy)
      · exact add_lt_add_left (oy.1 iy jy) ⟨xl, xr, xL, xR⟩, by
      constructor
      · rintro (ix | iy)
        · exact (ox.moveLeft ix).add oy
        · exact ox.add (oy.moveLeft iy)
      · rintro (jx | jy)
        · apply (ox.moveRight jx).add oy
        · apply ox.add (oy.moveRight jy)⟩
termination_by x y => (x, y)

Proof state:
case right.inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : (PGame.mk xl xr xL xR).Numeric
oy : (PGame.mk yl yr yL yR).Numeric
jy : 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 := PGame.mk yl yr yL yR;
                        PGame.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)
                  (xR a))
              i (PGame.mk yl yr yL yR))
          (fun a =>
            rec
              (fun yl yr yL yR IHyl IHyr =>
                let_fun y := PGame.mk yl yr yL yR;
                PGame.mk (xl ⊕ yl) (xr ⊕ 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 := PGame.mk yl yr yL yR;
                                    PGame.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)
                              (xL 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 := PGame.mk yl yr yL yR;
                                  PGame.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)
                            (xR a))
                        i y)
                    IHyr t)
              (yR a))
          t)
      (Sum.inr jy)).Numeric

Tactic:
apply ox.add (oy.moveRight jy)

Result:
no goals

Proof state:
case right.inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
ox : (PGame.mk xl xr xL xR).Numeric
oy : (PGame.mk yl yr yL yR).Numeric
jx : xr
⊢ ((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 := PGame.mk yl yr yL yR;
                        PGame.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)
                  (xR a))
              i (PGame.mk yl yr yL yR))
          (fun a =>
            rec
              (fun yl yr yL yR IHyl IHyr =>
                let_fun y := PGame.mk yl yr yL yR;
                PGame.mk (xl ⊕ yl) (xr ⊕ 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 := PGame.mk yl yr yL yR;
                                    PGame.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)
                              (xL 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 := PGame.mk yl yr yL yR;
                                  PGame.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)
                            (xR a))
                        i y)
                    IHyr t)
              (yR a))
          t)
      (Sum.inl jx)).Numeric

Tactic:
apply (ox.moveRight jx).add oy

Result:
no goals