-- Mathlib/SetTheory/Game/PGame.lean
theorem Equiv.of_equiv {x y : PGame} (L : x.LeftMoves ≃ y.LeftMoves)
    (R : x.RightMoves ≃ y.RightMoves) (hl : ∀ i, x.moveLeft i ≈ y.moveLeft (L i))
    (hr : ∀ j, x.moveRight j ≈ y.moveRight (R j)) : x ≈ y

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

case hr₁
x y : PGame
L : x.LeftMoves ≃ y.LeftMoves
R : x.RightMoves ≃ y.RightMoves
hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)
hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)
i : x.RightMoves
⊢ ∃ j, x.moveRight i ≈ y.moveRight j

case hl₂
x y : PGame
L : x.LeftMoves ≃ y.LeftMoves
R : x.RightMoves ≃ y.RightMoves
hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)
hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)
i : y.LeftMoves
⊢ ∃ i_1, x.moveLeft i_1 ≈ y.moveLeft i

case hr₂
x y : PGame
L : x.LeftMoves ≃ y.LeftMoves
R : x.RightMoves ≃ y.RightMoves
hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)
hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)
i : y.RightMoves
⊢ ∃ i_1, x.moveRight i_1 ≈ y.moveRight i

Tactic:
exacts [⟨_, hl i⟩, ⟨_, hr i⟩,
  ⟨_, by simpa using hl (L.symm i)⟩, ⟨_, by simpa using hr (R.symm i)⟩]

Result:
no goals

Proof state:
x y : PGame
L : x.LeftMoves ≃ y.LeftMoves
R : x.RightMoves ≃ y.RightMoves
hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)
hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)
i : y.LeftMoves
⊢ x.moveLeft ?m.85824 ≈ y.moveLeft i

Tactic:
simpa using hl (L.symm i)

Result:
no goals

Proof state:
x y : PGame
L : x.LeftMoves ≃ y.LeftMoves
R : x.RightMoves ≃ y.RightMoves
hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)
hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)
⊢ x ≈ y

Tactic:
apply Equiv.of_exists <;> intro i

Result:
case hl₁
x y : PGame
L : x.LeftMoves ≃ y.LeftMoves
R : x.RightMoves ≃ y.RightMoves
hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)
hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)
i : x.LeftMoves
⊢ ∃ j, x.moveLeft i ≈ y.moveLeft j

case hr₁
x y : PGame
L : x.LeftMoves ≃ y.LeftMoves
R : x.RightMoves ≃ y.RightMoves
hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)
hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)
i : x.RightMoves
⊢ ∃ j, x.moveRight i ≈ y.moveRight j

case hl₂
x y : PGame
L : x.LeftMoves ≃ y.LeftMoves
R : x.RightMoves ≃ y.RightMoves
hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)
hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)
i : y.LeftMoves
⊢ ∃ i_1, x.moveLeft i_1 ≈ y.moveLeft i

case hr₂
x y : PGame
L : x.LeftMoves ≃ y.LeftMoves
R : x.RightMoves ≃ y.RightMoves
hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)
hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)
i : y.RightMoves
⊢ ∃ i_1, x.moveRight i_1 ≈ y.moveRight i

Proof state:
x y : PGame
L : x.LeftMoves ≃ y.LeftMoves
R : x.RightMoves ≃ y.RightMoves
hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)
hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)
i : y.RightMoves
⊢ x.moveRight ?m.86055 ≈ y.moveRight i

Tactic:
simpa using hr (R.symm i)

Result:
no goals