-- Mathlib/SetTheory/Surreal/Basic.lean
theorem lf_asymm {x y : PGame} (ox : Numeric x) (oy : Numeric y) : x ⧏ y → ¬y ⧏ x

Proof state:
x y : PGame
ox : x.Numeric
oy : y.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), (xL i).Numeric
_oxr : ∀ (i : xr), (xR i).Numeric
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), (yL i).Numeric
oyr : ∀ (i : yr), (yR i).Numeric
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
⊢ ((∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR) →
    ¬((∃ i, mk yl yr yL yR ≤ xL i) ∨ ∃ j, yR j ≤ mk xl xr xL xR)

Tactic:
rintro (⟨i, h₁⟩ | ⟨j, h₁⟩) (⟨i, h₂⟩ | ⟨j, h₂⟩)

Result:
case inl.intro.inl.intro
x y : PGame
ox : x.Numeric
oy : y.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), (xL i).Numeric
_oxr : ∀ (i : xr), (xR i).Numeric
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), (yL i).Numeric
oyr : ∀ (i : yr), (yR i).Numeric
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
i✝ : yl
h₁ : mk xl xr xL xR ≤ yL i✝
i : xl
h₂ : mk yl yr yL yR ≤ xL i
⊢ False

case inl.intro.inr.intro
x y : PGame
ox : x.Numeric
oy : y.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), (xL i).Numeric
_oxr : ∀ (i : xr), (xR i).Numeric
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), (yL i).Numeric
oyr : ∀ (i : yr), (yR i).Numeric
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
i : yl
h₁ : mk xl xr xL xR ≤ yL i
j : yr
h₂ : yR j ≤ mk xl xr xL xR
⊢ False

case inr.intro.inl.intro
x y : PGame
ox : x.Numeric
oy : y.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), (xL i).Numeric
_oxr : ∀ (i : xr), (xR i).Numeric
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), (yL i).Numeric
oyr : ∀ (i : yr), (yR i).Numeric
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
j : xr
h₁ : xR j ≤ mk yl yr yL yR
i : xl
h₂ : mk yl yr yL yR ≤ xL i
⊢ False

case inr.intro.inr.intro
x y : PGame
ox : x.Numeric
oy : y.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), (xL i).Numeric
_oxr : ∀ (i : xr), (xR i).Numeric
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), (yL i).Numeric
oyr : ∀ (i : yr), (yR i).Numeric
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
j✝ : xr
h₁ : xR j✝ ≤ mk yl yr yL yR
j : yr
h₂ : yR j ≤ mk xl xr xL xR
⊢ False

Proof state:
x y : PGame
ox : x.Numeric
oy : y.Numeric
⊢ x ⧏ y → ¬y ⧏ x

Tactic:
refine numeric_rec (C := fun x => ∀ z (_oz : Numeric z), x ⧏ z → ¬z ⧏ x)
  (fun xl xr xL xR hx _oxl _oxr IHxl IHxr => ?_) x ox y oy

Result:
x y : PGame
ox : x.Numeric
oy : y.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), (xL i).Numeric
_oxr : ∀ (i : xr), (xR i).Numeric
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)
⊢ (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (mk xl xr xL xR)

Proof state:
case inl.intro.inl.intro
x y : PGame
ox : x.Numeric
oy : y.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), (xL i).Numeric
_oxr : ∀ (i : xr), (xR i).Numeric
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), (yL i).Numeric
oyr : ∀ (i : yr), (yR i).Numeric
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
i✝ : yl
h₁ : mk xl xr xL xR ≤ yL i✝
i : xl
h₂ : mk yl yr yL yR ≤ xL i
⊢ False

Tactic:
exact IHxl _ _ (oyl _) (h₁.moveLeft_lf _) (h₂.moveLeft_lf _)

Result:
no goals

Proof state:
case inr.intro.inr.intro
x y : PGame
ox : x.Numeric
oy : y.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), (xL i).Numeric
_oxr : ∀ (i : xr), (xR i).Numeric
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), (yL i).Numeric
oyr : ∀ (i : yr), (yR i).Numeric
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
j✝ : xr
h₁ : xR j✝ ≤ mk yl yr yL yR
j : yr
h₂ : yR j ≤ mk xl xr xL xR
⊢ False

Tactic:
exact IHxr _ _ (oyr _) (h₁.lf_moveRight _) (h₂.lf_moveRight _)

Result:
no goals

Proof state:
case inr.intro.inl.intro
x y : PGame
ox : x.Numeric
oy : y.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), (xL i).Numeric
_oxr : ∀ (i : xr), (xR i).Numeric
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), (yL i).Numeric
oyr : ∀ (i : yr), (yR i).Numeric
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
j : xr
h₁ : xR j ≤ mk yl yr yL yR
i : xl
h₂ : mk yl yr yL yR ≤ xL i
⊢ False

Tactic:
exact (le_trans h₁ h₂).not_gf (lf_of_lt (hx _ _))

Result:
no goals

Proof state:
case inl.intro.inr.intro
x y : PGame
ox : x.Numeric
oy : y.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), (xL i).Numeric
_oxr : ∀ (i : xr), (xR i).Numeric
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), (yL i).Numeric
oyr : ∀ (i : yr), (yR i).Numeric
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
i : yl
h₁ : mk xl xr xL xR ≤ yL i
j : yr
h₂ : yR j ≤ mk xl xr xL xR
⊢ False

Tactic:
exact (le_trans h₂ h₁).not_gf (lf_of_lt (hy _ _))

Result:
no goals