-- Mathlib/SetTheory/Game/PGame.lean
lemma ext {x y : PGame} (hl : x.LeftMoves = y.LeftMoves) (hr : x.RightMoves = y.RightMoves)
    (hL : ∀ i j, HEq i j → x.moveLeft i = y.moveLeft j)
    (hR : ∀ i j, HEq i j → x.moveRight i = y.moveRight j) :
    x = y

Proof state:
case mk.mk
α✝ β✝ : Type u_1
a✝³ : α✝ → PGame
a✝² : β✝ → PGame
a✝¹ : (mk α✝ β✝ a✝³ a✝²).LeftMoves → PGame
a✝ : (mk α✝ β✝ a✝³ a✝²).RightMoves → PGame
hL :
  ∀ (i : (mk α✝ β✝ a✝³ a✝²).LeftMoves)
    (j : (mk (mk α✝ β✝ a✝³ a✝²).LeftMoves (mk α✝ β✝ a✝³ a✝²).RightMoves a✝¹ a✝).LeftMoves),
    HEq i j →
      (mk α✝ β✝ a✝³ a✝²).moveLeft i = (mk (mk α✝ β✝ a✝³ a✝²).LeftMoves (mk α✝ β✝ a✝³ a✝²).RightMoves a✝¹ a✝).moveLeft j
hR :
  ∀ (i : (mk α✝ β✝ a✝³ a✝²).RightMoves)
    (j : (mk (mk α✝ β✝ a✝³ a✝²).LeftMoves (mk α✝ β✝ a✝³ a✝²).RightMoves a✝¹ a✝).RightMoves),
    HEq i j →
      (mk α✝ β✝ a✝³ a✝²).moveRight i =
        (mk (mk α✝ β✝ a✝³ a✝²).LeftMoves (mk α✝ β✝ a✝³ a✝²).RightMoves a✝¹ a✝).moveRight j
⊢ mk α✝ β✝ a✝³ a✝² = mk (mk α✝ β✝ a✝³ a✝²).LeftMoves (mk α✝ β✝ a✝³ a✝²).RightMoves a✝¹ a✝

Tactic:
simp only [leftMoves_mk, rightMoves_mk, heq_eq_eq, forall_eq', mk.injEq, true_and] at *

Result:
case mk.mk
α✝ β✝ : Type u_1
a✝³ : α✝ → PGame
a✝² : β✝ → PGame
a✝¹ : (mk α✝ β✝ a✝³ a✝²).LeftMoves → PGame
a✝ : (mk α✝ β✝ a✝³ a✝²).RightMoves → PGame
hL : ∀ (i : α✝), (mk α✝ β✝ a✝³ a✝²).moveLeft i = (mk α✝ β✝ a✝¹ a✝).moveLeft i
hR : ∀ (i : β✝), (mk α✝ β✝ a✝³ a✝²).moveRight i = (mk α✝ β✝ a✝¹ a✝).moveRight i
⊢ a✝³ = a✝¹ ∧ a✝² = a✝

Proof state:
case mk.mk
α✝ β✝ : Type u_1
a✝³ : α✝ → PGame
a✝² : β✝ → PGame
a✝¹ : (mk α✝ β✝ a✝³ a✝²).LeftMoves → PGame
a✝ : (mk α✝ β✝ a✝³ a✝²).RightMoves → PGame
hL : ∀ (i : α✝), (mk α✝ β✝ a✝³ a✝²).moveLeft i = (mk α✝ β✝ a✝¹ a✝).moveLeft i
hR : ∀ (i : β✝), (mk α✝ β✝ a✝³ a✝²).moveRight i = (mk α✝ β✝ a✝¹ a✝).moveRight i
⊢ a✝³ = a✝¹ ∧ a✝² = a✝

Tactic:
exact ⟨funext hL, funext hR⟩

Result:
no goals

Proof state:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
hl : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves = (mk α✝ β✝ a✝¹ a✝).LeftMoves
hr : (mk α✝¹ β✝¹ a✝³ a✝²).RightMoves = (mk α✝ β✝ a✝¹ a✝).RightMoves
hL :
  ∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
    HEq i j → (mk α✝¹ β✝¹ a✝³ a✝²).moveLeft i = (mk α✝ β✝ a✝¹ a✝).moveLeft j
hR :
  ∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).RightMoves) (j : (mk α✝ β✝ a✝¹ a✝).RightMoves),
    HEq i j → (mk α✝¹ β✝¹ a✝³ a✝²).moveRight i = (mk α✝ β✝ a✝¹ a✝).moveRight j
⊢ mk α✝¹ β✝¹ a✝³ a✝² = mk α✝ β✝ a✝¹ a✝

Tactic:
subst hl hr

Result:
case mk.mk
α✝ β✝ : Type u_1
a✝³ : α✝ → PGame
a✝² : β✝ → PGame
a✝¹ : (mk α✝ β✝ a✝³ a✝²).LeftMoves → PGame
a✝ : (mk α✝ β✝ a✝³ a✝²).RightMoves → PGame
hL :
  ∀ (i : (mk α✝ β✝ a✝³ a✝²).LeftMoves)
    (j : (mk (mk α✝ β✝ a✝³ a✝²).LeftMoves (mk α✝ β✝ a✝³ a✝²).RightMoves a✝¹ a✝).LeftMoves),
    HEq i j →
      (mk α✝ β✝ a✝³ a✝²).moveLeft i = (mk (mk α✝ β✝ a✝³ a✝²).LeftMoves (mk α✝ β✝ a✝³ a✝²).RightMoves a✝¹ a✝).moveLeft j
hR :
  ∀ (i : (mk α✝ β✝ a✝³ a✝²).RightMoves)
    (j : (mk (mk α✝ β✝ a✝³ a✝²).LeftMoves (mk α✝ β✝ a✝³ a✝²).RightMoves a✝¹ a✝).RightMoves),
    HEq i j →
      (mk α✝ β✝ a✝³ a✝²).moveRight i =
        (mk (mk α✝ β✝ a✝³ a✝²).LeftMoves (mk α✝ β✝ a✝³ a✝²).RightMoves a✝¹ a✝).moveRight j
⊢ mk α✝ β✝ a✝³ a✝² = mk (mk α✝ β✝ a✝³ a✝²).LeftMoves (mk α✝ β✝ a✝³ a✝²).RightMoves a✝¹ a✝

Proof state:
case mk
y : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
hl : (mk α✝ β✝ a✝¹ a✝).LeftMoves = y.LeftMoves
hr : (mk α✝ β✝ a✝¹ a✝).RightMoves = y.RightMoves
hL : ∀ (i : (mk α✝ β✝ a✝¹ a✝).LeftMoves) (j : y.LeftMoves), HEq i j → (mk α✝ β✝ a✝¹ a✝).moveLeft i = y.moveLeft j
hR : ∀ (i : (mk α✝ β✝ a✝¹ a✝).RightMoves) (j : y.RightMoves), HEq i j → (mk α✝ β✝ a✝¹ a✝).moveRight i = y.moveRight j
⊢ mk α✝ β✝ a✝¹ a✝ = y

Tactic:
cases y

Result:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
hl : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves = (mk α✝ β✝ a✝¹ a✝).LeftMoves
hr : (mk α✝¹ β✝¹ a✝³ a✝²).RightMoves = (mk α✝ β✝ a✝¹ a✝).RightMoves
hL :
  ∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
    HEq i j → (mk α✝¹ β✝¹ a✝³ a✝²).moveLeft i = (mk α✝ β✝ a✝¹ a✝).moveLeft j
hR :
  ∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).RightMoves) (j : (mk α✝ β✝ a✝¹ a✝).RightMoves),
    HEq i j → (mk α✝¹ β✝¹ a✝³ a✝²).moveRight i = (mk α✝ β✝ a✝¹ a✝).moveRight j
⊢ mk α✝¹ β✝¹ a✝³ a✝² = mk α✝ β✝ a✝¹ a✝

Proof state:
x y : PGame
hl : x.LeftMoves = y.LeftMoves
hr : x.RightMoves = y.RightMoves
hL : ∀ (i : x.LeftMoves) (j : y.LeftMoves), HEq i j → x.moveLeft i = y.moveLeft j
hR : ∀ (i : x.RightMoves) (j : y.RightMoves), HEq i j → x.moveRight i = y.moveRight j
⊢ x = y

Tactic:
cases x

Result:
case mk
y : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
hl : (mk α✝ β✝ a✝¹ a✝).LeftMoves = y.LeftMoves
hr : (mk α✝ β✝ a✝¹ a✝).RightMoves = y.RightMoves
hL : ∀ (i : (mk α✝ β✝ a✝¹ a✝).LeftMoves) (j : y.LeftMoves), HEq i j → (mk α✝ β✝ a✝¹ a✝).moveLeft i = y.moveLeft j
hR : ∀ (i : (mk α✝ β✝ a✝¹ a✝).RightMoves) (j : y.RightMoves), HEq i j → (mk α✝ β✝ a✝¹ a✝).moveRight i = y.moveRight j
⊢ mk α✝ β✝ a✝¹ a✝ = y