-- Mathlib/SetTheory/Surreal/Basic.lean
theorem insertLeft_numeric {x x' : PGame} (x_num : x.Numeric) (x'_num : x'.Numeric)
    (h : x' ≤ x) : (insertLeft x x').Numeric

Proof state:
case mk.left
x' : PGame
x'_num : x'.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : (∀ (i : x'.LeftMoves), x'.moveLeft i < mk xl xr xL xR) ∧ ∀ (j : xr), x' < xR j
x_num : (∀ (i : xl) (j : xr), xL i < xR j) ∧ (∀ (i : xl), (xL i).Numeric) ∧ ∀ (j : xr), (xR j).Numeric
⊢ ∀ (j : xr), x' < xR j

Tactic:
exact h.2

Result:
no goals

Proof state:
x x' : PGame
x_num : x.Numeric
x'_num : x'.Numeric
h : (∀ (i : x'.LeftMoves), x'.moveLeft i < x) ∧ ∀ (j : x.RightMoves), x' < x.moveRight j
⊢ (x.insertLeft x').Numeric

Tactic:
unfold Numeric at x_num ⊢

Result:
x x' : PGame
x'_num : x'.Numeric
h : (∀ (i : x'.LeftMoves), x'.moveLeft i < x) ∧ ∀ (j : x.RightMoves), x' < x.moveRight j
x_num :
  match x with
  | mk α β L R => (∀ (i : α) (j : β), L i < R j) ∧ (∀ (i : α), (L i).Numeric) ∧ ∀ (j : β), (R j).Numeric
⊢ match x.insertLeft x' with
  | mk α β L R => (∀ (i : α) (j : β), L i < R j) ∧ (∀ (i : α), (L i).Numeric) ∧ ∀ (j : β), (R j).Numeric

Proof state:
case mk.left
x' : PGame
x'_num : x'.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h :
  (∀ (i : x'.LeftMoves), x'.moveLeft i < mk xl xr xL xR) ∧
    ∀ (j : (mk xl xr xL xR).RightMoves), x' < (mk xl xr xL xR).moveRight j
x_num : (∀ (i : xl) (j : xr), xL i < xR j) ∧ (∀ (i : xl), (xL i).Numeric) ∧ ∀ (j : xr), (xR j).Numeric
⊢ ∀ (j : xr), x' < xR j

Tactic:
simp only [rightMoves_mk, moveRight_mk] at h

Result:
case mk.left
x' : PGame
x'_num : x'.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h : (∀ (i : x'.LeftMoves), x'.moveLeft i < mk xl xr xL xR) ∧ ∀ (j : xr), x' < xR j
x_num : (∀ (i : xl) (j : xr), xL i < xR j) ∧ (∀ (i : xl), (xL i).Numeric) ∧ ∀ (j : xr), (xR j).Numeric
⊢ ∀ (j : xr), x' < xR j

Proof state:
x x' : PGame
x_num : x.Numeric
x'_num : x'.Numeric
h : x' ≤ x
⊢ (x.insertLeft x').Numeric

Tactic:
rw [le_iff_forall_lt x'_num x_num] at h

Result:
x x' : PGame
x_num : x.Numeric
x'_num : x'.Numeric
h : (∀ (i : x'.LeftMoves), x'.moveLeft i < x) ∧ ∀ (j : x.RightMoves), x' < x.moveRight j
⊢ (x.insertLeft x').Numeric

Proof state:
case mk
x' : PGame
x'_num : x'.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h :
  (∀ (i : x'.LeftMoves), x'.moveLeft i < mk xl xr xL xR) ∧
    ∀ (j : (mk xl xr xL xR).RightMoves), x' < (mk xl xr xL xR).moveRight j
x_num : (∀ (i : xl) (j : xr), xL i < xR j) ∧ (∀ (i : xl), (xL i).Numeric) ∧ ∀ (j : xr), (xR j).Numeric
⊢ ((∀ (a : xl) (j : xr), xL a < xR j) ∧ ∀ (j : xr), x' < xR j) ∧
    ((∀ (a : xl), (xL a).Numeric) ∧ x'.Numeric) ∧ ∀ (j : xr), (xR j).Numeric

Tactic:
constructor

Result:
case mk.left
x' : PGame
x'_num : x'.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h :
  (∀ (i : x'.LeftMoves), x'.moveLeft i < mk xl xr xL xR) ∧
    ∀ (j : (mk xl xr xL xR).RightMoves), x' < (mk xl xr xL xR).moveRight j
x_num : (∀ (i : xl) (j : xr), xL i < xR j) ∧ (∀ (i : xl), (xL i).Numeric) ∧ ∀ (j : xr), (xR j).Numeric
⊢ (∀ (a : xl) (j : xr), xL a < xR j) ∧ ∀ (j : xr), x' < xR j

case mk.right
x' : PGame
x'_num : x'.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h :
  (∀ (i : x'.LeftMoves), x'.moveLeft i < mk xl xr xL xR) ∧
    ∀ (j : (mk xl xr xL xR).RightMoves), x' < (mk xl xr xL xR).moveRight j
x_num : (∀ (i : xl) (j : xr), xL i < xR j) ∧ (∀ (i : xl), (xL i).Numeric) ∧ ∀ (j : xr), (xR j).Numeric
⊢ ((∀ (a : xl), (xL a).Numeric) ∧ x'.Numeric) ∧ ∀ (j : xr), (xR j).Numeric

Proof state:
case mk.right
x' : PGame
x'_num : x'.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h :
  (∀ (i : x'.LeftMoves), x'.moveLeft i < mk xl xr xL xR) ∧
    ∀ (j : (mk xl xr xL xR).RightMoves), x' < (mk xl xr xL xR).moveRight j
x_num : (∀ (i : xl) (j : xr), xL i < xR j) ∧ (∀ (i : xl), (xL i).Numeric) ∧ ∀ (j : xr), (xR j).Numeric
⊢ ((∀ (a : xl), (xL a).Numeric) ∧ x'.Numeric) ∧ ∀ (j : xr), (xR j).Numeric

Tactic:
simp only [x_num, implies_true, x'_num, and_self]

Result:
no goals

Proof state:
case mk.left
x' : PGame
x'_num : x'.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h :
  (∀ (i : x'.LeftMoves), x'.moveLeft i < mk xl xr xL xR) ∧
    ∀ (j : (mk xl xr xL xR).RightMoves), x' < (mk xl xr xL xR).moveRight j
x_num : (∀ (i : xl) (j : xr), xL i < xR j) ∧ (∀ (i : xl), (xL i).Numeric) ∧ ∀ (j : xr), (xR j).Numeric
⊢ (∀ (a : xl) (j : xr), xL a < xR j) ∧ ∀ (j : xr), x' < xR j

Tactic:
simp only [x_num.1, implies_true, true_and]

Result:
case mk.left
x' : PGame
x'_num : x'.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h :
  (∀ (i : x'.LeftMoves), x'.moveLeft i < mk xl xr xL xR) ∧
    ∀ (j : (mk xl xr xL xR).RightMoves), x' < (mk xl xr xL xR).moveRight j
x_num : (∀ (i : xl) (j : xr), xL i < xR j) ∧ (∀ (i : xl), (xL i).Numeric) ∧ ∀ (j : xr), (xR j).Numeric
⊢ ∀ (j : xr), x' < xR j

Proof state:
case mk
x' : PGame
x'_num : x'.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h :
  (∀ (i : x'.LeftMoves), x'.moveLeft i < mk xl xr xL xR) ∧
    ∀ (j : (mk xl xr xL xR).RightMoves), x' < (mk xl xr xL xR).moveRight j
x_num :
  match mk xl xr xL xR with
  | mk α β L R => (∀ (i : α) (j : β), L i < R j) ∧ (∀ (i : α), (L i).Numeric) ∧ ∀ (j : β), (R j).Numeric
⊢ match (mk xl xr xL xR).insertLeft x' with
  | mk α β L R => (∀ (i : α) (j : β), L i < R j) ∧ (∀ (i : α), (L i).Numeric) ∧ ∀ (j : β), (R j).Numeric

Tactic:
simp only [insertLeft, Sum.forall, forall_const, Sum.elim_inl, Sum.elim_inr] at x_num ⊢

Result:
case mk
x' : PGame
x'_num : x'.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h :
  (∀ (i : x'.LeftMoves), x'.moveLeft i < mk xl xr xL xR) ∧
    ∀ (j : (mk xl xr xL xR).RightMoves), x' < (mk xl xr xL xR).moveRight j
x_num : (∀ (i : xl) (j : xr), xL i < xR j) ∧ (∀ (i : xl), (xL i).Numeric) ∧ ∀ (j : xr), (xR j).Numeric
⊢ ((∀ (a : xl) (j : xr), xL a < xR j) ∧ ∀ (j : xr), x' < xR j) ∧
    ((∀ (a : xl), (xL a).Numeric) ∧ x'.Numeric) ∧ ∀ (j : xr), (xR j).Numeric

Proof state:
x x' : PGame
x'_num : x'.Numeric
h : (∀ (i : x'.LeftMoves), x'.moveLeft i < x) ∧ ∀ (j : x.RightMoves), x' < x.moveRight j
x_num :
  match x with
  | mk α β L R => (∀ (i : α) (j : β), L i < R j) ∧ (∀ (i : α), (L i).Numeric) ∧ ∀ (j : β), (R j).Numeric
⊢ match x.insertLeft x' with
  | mk α β L R => (∀ (i : α) (j : β), L i < R j) ∧ (∀ (i : α), (L i).Numeric) ∧ ∀ (j : β), (R j).Numeric

Tactic:
rcases x with ⟨xl, xr, xL, xR⟩

Result:
case mk
x' : PGame
x'_num : x'.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h :
  (∀ (i : x'.LeftMoves), x'.moveLeft i < mk xl xr xL xR) ∧
    ∀ (j : (mk xl xr xL xR).RightMoves), x' < (mk xl xr xL xR).moveRight j
x_num :
  match mk xl xr xL xR with
  | mk α β L R => (∀ (i : α) (j : β), L i < R j) ∧ (∀ (i : α), (L i).Numeric) ∧ ∀ (j : β), (R j).Numeric
⊢ match (mk xl xr xL xR).insertLeft x' with
  | mk α β L R => (∀ (i : α) (j : β), L i < R j) ∧ (∀ (i : α), (L i).Numeric) ∧ ∀ (j : β), (R j).Numeric