case inl.inl
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x < y ∨ (x ≈ y) ∨ y < x ∨ x ‖ y

case inl.inr
x y : PGame
h₁ : x ≤ y
h₂ : x ⧏ y
⊢ x < y ∨ (x ≈ y) ∨ y < x ∨ x ‖ y

case inr.inl
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ x < y ∨ (x ≈ y) ∨ y < x ∨ x ‖ y

case inr.inr
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ x < y ∨ (x ≈ y) ∨ y < x ∨ x ‖ y
x y : PGame
⊢ x < y ∨ (x ≈ y) ∨ y < x ∨ x ‖ y
cases' le_or_gf x y with h₁ h₁ <;> cases' le_or_gf y x with h₂ h₂
case inl.inl.h
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ (x ≈ y) ∨ y < x ∨ x ‖ y
case inl.inl
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x < y ∨ (x ≈ y) ∨ y < x ∨ x ‖ y
right
case inl.inl.h.h
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x ≈ y
case inl.inl.h
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ (x ≈ y) ∨ y < x ∨ x ‖ y
left
no goals
case inl.inl.h.h
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x ≈ y
exact ⟨h₁, h₂⟩
case inl.inr.h
x y : PGame
h₁ : x ≤ y
h₂ : x ⧏ y
⊢ x < y
case inl.inr
x y : PGame
h₁ : x ≤ y
h₂ : x ⧏ y
⊢ x < y ∨ (x ≈ y) ∨ y < x ∨ x ‖ y
left
no goals
case inl.inr.h
x y : PGame
h₁ : x ≤ y
h₂ : x ⧏ y
⊢ x < y
exact ⟨h₁, h₂⟩
case inr.inl.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ (x ≈ y) ∨ y < x ∨ x ‖ y
case inr.inl
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ x < y ∨ (x ≈ y) ∨ y < x ∨ x ‖ y
right
case inr.inl.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ y < x ∨ x ‖ y
case inr.inl.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ (x ≈ y) ∨ y < x ∨ x ‖ y
right
case inr.inl.h.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ y < x
case inr.inl.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ y < x ∨ x ‖ y
left
no goals
case inr.inl.h.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ y < x
exact ⟨h₂, h₁⟩
case inr.inr.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ (x ≈ y) ∨ y < x ∨ x ‖ y
case inr.inr
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ x < y ∨ (x ≈ y) ∨ y < x ∨ x ‖ y
right
case inr.inr.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ y < x ∨ x ‖ y
case inr.inr.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ (x ≈ y) ∨ y < x ∨ x ‖ y
right
case inr.inr.h.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ x ‖ y
case inr.inr.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ y < x ∨ x ‖ y
right
no goals
case inr.inr.h.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ x ‖ y
exact ⟨h₂, h₁⟩