-- Mathlib/SetTheory/Game/PGame.lean
theorem Equiv.of_exists {x y : PGame}
    (hl₁ : ∀ i, ∃ j, x.moveLeft i ≈ y.moveLeft j) (hr₁ : ∀ i, ∃ j, x.moveRight i ≈ y.moveRight j)
    (hl₂ : ∀ j, ∃ i, x.moveLeft i ≈ y.moveLeft j) (hr₂ : ∀ j, ∃ i, x.moveRight i ≈ y.moveRight j) :
    x ≈ y

Proof state:
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
⊢ x ≈ y

Tactic:
constructor <;> refine le_def.2 ⟨?_, ?_⟩ <;> intro i

Result:
case left.refine_1
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : x.LeftMoves
⊢ (∃ i', x.moveLeft i ≤ y.moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ y

case left.refine_2
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : y.RightMoves
⊢ (∃ i_1, x ≤ (y.moveRight i).moveLeft i_1) ∨ ∃ j', x.moveRight j' ≤ y.moveRight i

case right.refine_1
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : y.LeftMoves
⊢ (∃ i', y.moveLeft i ≤ x.moveLeft i') ∨ ∃ j, (y.moveLeft i).moveRight j ≤ x

case right.refine_2
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : x.RightMoves
⊢ (∃ i_1, y ≤ (x.moveRight i).moveLeft i_1) ∨ ∃ j', y.moveRight j' ≤ x.moveRight i

Proof state:
case left.refine_1
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : x.LeftMoves
⊢ (∃ i', x.moveLeft i ≤ y.moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ y

Tactic:
obtain ⟨j, hj⟩ := hl₁ i

Result:
case left.refine_1.intro
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : x.LeftMoves
j : y.LeftMoves
hj : x.moveLeft i ≈ y.moveLeft j
⊢ (∃ i', x.moveLeft i ≤ y.moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ y

Proof state:
case left.refine_2.intro
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : y.RightMoves
j : x.RightMoves
hj : x.moveRight j ≈ y.moveRight i
⊢ (∃ i_1, x ≤ (y.moveRight i).moveLeft i_1) ∨ ∃ j', x.moveRight j' ≤ y.moveRight i

Tactic:
exact Or.inr ⟨j, Equiv.le hj⟩

Result:
no goals

Proof state:
case right.refine_1.intro
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : y.LeftMoves
j : x.LeftMoves
hj : x.moveLeft j ≈ y.moveLeft i
⊢ (∃ i', y.moveLeft i ≤ x.moveLeft i') ∨ ∃ j, (y.moveLeft i).moveRight j ≤ x

Tactic:
exact Or.inl ⟨j, Equiv.ge hj⟩

Result:
no goals

Proof state:
case left.refine_2
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : y.RightMoves
⊢ (∃ i_1, x ≤ (y.moveRight i).moveLeft i_1) ∨ ∃ j', x.moveRight j' ≤ y.moveRight i

Tactic:
obtain ⟨j, hj⟩ := hr₂ i

Result:
case left.refine_2.intro
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : y.RightMoves
j : x.RightMoves
hj : x.moveRight j ≈ y.moveRight i
⊢ (∃ i_1, x ≤ (y.moveRight i).moveLeft i_1) ∨ ∃ j', x.moveRight j' ≤ y.moveRight i

Proof state:
case right.refine_1
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : y.LeftMoves
⊢ (∃ i', y.moveLeft i ≤ x.moveLeft i') ∨ ∃ j, (y.moveLeft i).moveRight j ≤ x

Tactic:
obtain ⟨j, hj⟩ := hl₂ i

Result:
case right.refine_1.intro
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : y.LeftMoves
j : x.LeftMoves
hj : x.moveLeft j ≈ y.moveLeft i
⊢ (∃ i', y.moveLeft i ≤ x.moveLeft i') ∨ ∃ j, (y.moveLeft i).moveRight j ≤ x

Proof state:
case right.refine_2
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : x.RightMoves
⊢ (∃ i_1, y ≤ (x.moveRight i).moveLeft i_1) ∨ ∃ j', y.moveRight j' ≤ x.moveRight i

Tactic:
obtain ⟨j, hj⟩ := hr₁ i

Result:
case right.refine_2.intro
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : x.RightMoves
j : y.RightMoves
hj : x.moveRight i ≈ y.moveRight j
⊢ (∃ i_1, y ≤ (x.moveRight i).moveLeft i_1) ∨ ∃ j', y.moveRight j' ≤ x.moveRight i

Proof state:
case right.refine_2.intro
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : x.RightMoves
j : y.RightMoves
hj : x.moveRight i ≈ y.moveRight j
⊢ (∃ i_1, y ≤ (x.moveRight i).moveLeft i_1) ∨ ∃ j', y.moveRight j' ≤ x.moveRight i

Tactic:
exact Or.inr ⟨j, Equiv.ge hj⟩

Result:
no goals

Proof state:
case left.refine_1.intro
x y : PGame
hl₁ : ∀ (i : x.LeftMoves), ∃ j, x.moveLeft i ≈ y.moveLeft j
hr₁ : ∀ (i : x.RightMoves), ∃ j, x.moveRight i ≈ y.moveRight j
hl₂ : ∀ (j : y.LeftMoves), ∃ i, x.moveLeft i ≈ y.moveLeft j
hr₂ : ∀ (j : y.RightMoves), ∃ i, x.moveRight i ≈ y.moveRight j
i : x.LeftMoves
j : y.LeftMoves
hj : x.moveLeft i ≈ y.moveLeft j
⊢ (∃ i', x.moveLeft i ≤ y.moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ y

Tactic:
exact Or.inl ⟨j, Equiv.le hj⟩

Result:
no goals