-- Mathlib/SetTheory/Game/Short.lean
theorem subsingleton_short_example : ∀ x : PGame, Subsingleton (Short x)
  | mk xl xr xL xR =>
    ⟨fun a b => by
      cases a; cases b
      congr!
      · funext x
        apply @Subsingleton.elim _ (subsingleton_short_example (xL x))
        -- Decreasing goal in Lean 4 is `Subsequent (xL x) (mk α β L R)`
        -- where `α`, `β`, `L`, and `R` are fresh hypotheses only propositionally
        -- equal to `xl`, `xr`, `xL`, and `xR`.
        -- (In Lean 3 it was `(mk xl xr xL xR)` instead.)
      · funext x
        apply @Subsingleton.elim _ (subsingleton_short_example (xR x))⟩
termination_by x => x
-- We need to unify a bunch of hypotheses before `pgame_wf_tac` can work.
decreasing_by all_goals {
  subst_vars
  simp only [mk.injEq, heq_eq_eq, true_and] at *
  casesm* _ ∧ _
  subst_vars
  pgame_wf_tac
}

Proof state:
α✝ β✝ : Type u_1
L✝ : α✝ → PGame
R✝ : β✝ → PGame
L xL : α✝ → PGame
inst✝³ : Fintype α✝
x✝⁵ : (i : α✝) → (xL i).Short
inst✝² : Fintype α✝
x✝⁴ : (i : α✝) → (xL i).Short
R xR : β✝ → PGame
inst✝¹ : Fintype β✝
x✝³ : (j : β✝) → (xR j).Short
inst✝ : Fintype β✝
x✝² : (j : β✝) → (xR j).Short
x : β✝
x✝¹ : ∀ (y : PGame), (invImage (fun x => x) instWellFoundedRelation).1 y (mk α✝ β✝ L R) → Subsingleton y.Short
x✝ : ∀ (y : PGame), (invImage (fun x => x) instWellFoundedRelation).1 y (mk α✝ β✝ xL xR) → Subsingleton y.Short
h✝¹ : mk α✝ β✝ xL xR = mk α✝ β✝ L R
h✝ : mk α✝ β✝ xL xR = mk α✝ β✝ L✝ R✝
⊢ (xR x).Subsequent (mk α✝ β✝ L R)

Tactic:
simp only [mk.injEq, heq_eq_eq, true_and] at *

Result:
α✝ β✝ : Type u_1
L✝ : α✝ → PGame
R✝ : β✝ → PGame
L xL : α✝ → PGame
inst✝³ : Fintype α✝
x✝⁵ : (i : α✝) → (xL i).Short
inst✝² : Fintype α✝
x✝⁴ : (i : α✝) → (xL i).Short
R xR : β✝ → PGame
inst✝¹ : Fintype β✝
x✝³ : (j : β✝) → (xR j).Short
inst✝ : Fintype β✝
x✝² : (j : β✝) → (xR j).Short
x : β✝
x✝¹ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun x => x) y (mk α✝ β✝ L R) → Subsingleton y.Short
x✝ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun x => x) y (mk α✝ β✝ xL xR) → Subsingleton y.Short
h✝¹ : xL = L ∧ xR = R
h✝ : xL = L✝ ∧ xR = R✝
⊢ (xR x).Subsequent (mk α✝ β✝ L R)

Proof state:
case mk.mk
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
inst✝³ : Fintype xl
inst✝² : Fintype xr
x✝³ : (i : xl) → (xL i).Short
x✝² : (j : xr) → (xR j).Short
inst✝¹ : Fintype xl
inst✝ : Fintype xr
x✝¹ : (i : xl) → (xL i).Short
x✝ : (j : xr) → (xR j).Short
⊢ Short.mk x✝³ x✝² = Short.mk x✝¹ x✝

Tactic:
congr!

Result:
case mk.mk.h.e'_5
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
inst✝³ : Fintype xl
inst✝² : Fintype xr
x✝³ : (i : xl) → (xL i).Short
x✝² : (j : xr) → (xR j).Short
inst✝¹ : Fintype xl
inst✝ : Fintype xr
x✝¹ : (i : xl) → (xL i).Short
x✝ : (j : xr) → (xR j).Short
⊢ x✝³ = x✝¹

case mk.mk.h.e'_6
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
inst✝³ : Fintype xl
inst✝² : Fintype xr
x✝³ : (i : xl) → (xL i).Short
x✝² : (j : xr) → (xR j).Short
inst✝¹ : Fintype xl
inst✝ : Fintype xr
x✝¹ : (i : xl) → (xL i).Short
x✝ : (j : xr) → (xR j).Short
⊢ x✝² = x✝

Proof state:
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
a b : (mk xl xr xL xR).Short
⊢ a = b

Tactic:
cases a

Result:
case mk
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
b : (mk xl xr xL xR).Short
inst✝¹ : Fintype xl
inst✝ : Fintype xr
x✝¹ : (i : xl) → (xL i).Short
x✝ : (j : xr) → (xR j).Short
⊢ Short.mk x✝¹ x✝ = b

Proof state:
case intro.intro
α✝ β✝ : Type u_1
L✝ : α✝ → PGame
R✝ : β✝ → PGame
L xL : α✝ → PGame
inst✝³ : Fintype α✝
x✝⁵ : (i : α✝) → (xL i).Short
inst✝² : Fintype α✝
x✝⁴ : (i : α✝) → (xL i).Short
R xR : β✝ → PGame
inst✝¹ : Fintype β✝
x✝³ : (j : β✝) → (xR j).Short
inst✝ : Fintype β✝
x✝² : (j : β✝) → (xR j).Short
x : β✝
x✝¹ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun x => x) y (mk α✝ β✝ L R) → Subsingleton y.Short
x✝ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun x => x) y (mk α✝ β✝ xL xR) → Subsingleton y.Short
left✝¹ : xL = L
right✝¹ : xR = R
left✝ : xL = L✝
right✝ : xR = R✝
⊢ (xR x).Subsequent (mk α✝ β✝ L R)

Tactic:
subst_vars

Result:
case intro.intro
α✝ β✝ : Type u_1
xL : α✝ → PGame
inst✝³ : Fintype α✝
x✝⁵ : (i : α✝) → (xL i).Short
inst✝² : Fintype α✝
x✝⁴ : (i : α✝) → (xL i).Short
xR : β✝ → PGame
inst✝¹ : Fintype β✝
x✝³ : (j : β✝) → (xR j).Short
inst✝ : Fintype β✝
x✝² : (j : β✝) → (xR j).Short
x : β✝
x✝¹ x✝ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun x => x) y (mk α✝ β✝ xL xR) → Subsingleton y.Short
⊢ (xR x).Subsequent (mk α✝ β✝ xL xR)

Proof state:
case mk.mk.h.e'_6.h
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
inst✝³ : Fintype xl
inst✝² : Fintype xr
x✝³ : (i : xl) → (xL i).Short
x✝² : (j : xr) → (xR j).Short
inst✝¹ : Fintype xl
inst✝ : Fintype xr
x✝¹ : (i : xl) → (xL i).Short
x✝ : (j : xr) → (xR j).Short
x : xr
⊢ x✝² x = x✝ x

Tactic:
apply @Subsingleton.elim _ (subsingleton_short_example (xR x))

Result:
no goals

Proof state:
case intro.intro
α✝ β✝ : Type u_1
xL : α✝ → PGame
inst✝³ : Fintype α✝
x✝⁵ : (i : α✝) → (xL i).Short
inst✝² : Fintype α✝
x✝⁴ : (i : α✝) → (xL i).Short
xR : β✝ → PGame
inst✝¹ : Fintype β✝
x✝³ : (j : β✝) → (xR j).Short
inst✝ : Fintype β✝
x✝² : (j : β✝) → (xR j).Short
x : β✝
x✝¹ x✝ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun x => x) y (mk α✝ β✝ xL xR) → Subsingleton y.Short
⊢ (xR x).Subsequent (mk α✝ β✝ xL xR)

Tactic:
pgame_wf_tac

Result:
no goals

Proof state:
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
x✝⁵ : ∀ (y : PGame), (invImage (fun x => x) instWellFoundedRelation).1 y (mk xl xr xL xR) → Subsingleton y.Short
a b : (mk xl xr xL xR).Short
α β : Type u_1
L : α → PGame
R : β → PGame
x✝⁴ : ∀ (y : PGame), (invImage (fun x => x) instWellFoundedRelation).1 y (mk α β L R) → Subsingleton y.Short
h✝³ : mk xl xr xL xR = mk α β L R
α_eq✝¹ : xl = α
L✝² : xl → PGame
inst✝³ : Fintype xl
β_eq✝¹ : xr = β
R✝² : xr → PGame
inst✝² : Fintype xr
a_eq✝³ : HEq xL L✝²
x✝³ : (i : xl) → (xL i).Short
a_eq✝² : HEq xR R✝²
x✝² : (j : xr) → (xR j).Short
h✝² : HEq a (Short.mk x✝³ x✝²)
α✝ β✝ : Type u_1
L✝¹ : α✝ → PGame
R✝¹ : β✝ → PGame
h✝¹ : mk xl xr xL xR = mk α✝ β✝ L✝¹ R✝¹
α_eq✝ : xl = α✝
L✝ : xl → PGame
inst✝¹ : Fintype xl
β_eq✝ : xr = β✝
R✝ : xr → PGame
inst✝ : Fintype xr
a_eq✝¹ : HEq xL L✝
x✝¹ : (i : xl) → (xL i).Short
a_eq✝ : HEq xR R✝
x✝ : (j : xr) → (xR j).Short
h✝ : HEq b (Short.mk x✝¹ x✝)
x : xl
⊢ (xL x).Subsequent (mk α β L R)

xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
x✝⁵ : ∀ (y : PGame), (invImage (fun x => x) instWellFoundedRelation).1 y (mk xl xr xL xR) → Subsingleton y.Short
a b : (mk xl xr xL xR).Short
α β : Type u_1
L : α → PGame
R : β → PGame
x✝⁴ : ∀ (y : PGame), (invImage (fun x => x) instWellFoundedRelation).1 y (mk α β L R) → Subsingleton y.Short
h✝³ : mk xl xr xL xR = mk α β L R
α_eq✝¹ : xl = α
L✝² : xl → PGame
inst✝³ : Fintype xl
β_eq✝¹ : xr = β
R✝² : xr → PGame
inst✝² : Fintype xr
a_eq✝³ : HEq xL L✝²
x✝³ : (i : xl) → (xL i).Short
a_eq✝² : HEq xR R✝²
x✝² : (j : xr) → (xR j).Short
h✝² : HEq a (Short.mk x✝³ x✝²)
α✝ β✝ : Type u_1
L✝¹ : α✝ → PGame
R✝¹ : β✝ → PGame
h✝¹ : mk xl xr xL xR = mk α✝ β✝ L✝¹ R✝¹
α_eq✝ : xl = α✝
L✝ : xl → PGame
inst✝¹ : Fintype xl
β_eq✝ : xr = β✝
R✝ : xr → PGame
inst✝ : Fintype xr
a_eq✝¹ : HEq xL L✝
x✝¹ : (i : xl) → (xL i).Short
a_eq✝ : HEq xR R✝
x✝ : (j : xr) → (xR j).Short
h✝ : HEq b (Short.mk x✝¹ x✝)
x : xr
⊢ (xR x).Subsequent (mk α β L R)

Tactic:
all_goals {
subst_vars
simp only [mk.injEq, heq_eq_eq, true_and] at *
casesm* _ ∧ _
subst_vars
pgame_wf_tac
}

Result:
no goals