[GOAL]
x : PGame
⊢ Subsingleton (Short x)
[PROOFSTEP]
induction x with
| mk xl xr xL xR =>
  constructor
  intro a b
  cases a; cases b
  congr!
    -- Porting note: We use `induction` to prove `subsingleton_short` instead of recursion.
    -- A proof using recursion generates a harder `decreasing_by` goal than in Lean 3 for some reason:
[GOAL]
x : PGame
⊢ Subsingleton (Short x)
[PROOFSTEP]
induction x with
| mk xl xr xL xR =>
  constructor
  intro a b
  cases a; cases b
  congr!
    -- Porting note: We use `induction` to prove `subsingleton_short` instead of recursion.
    -- A proof using recursion generates a harder `decreasing_by` goal than in Lean 3 for some reason:
[GOAL]
case mk
xl xr : Type ?u.940
xL : xl → PGame
xR : xr → PGame
a_ih✝¹ : ∀ (a : xl), Subsingleton (Short (xL a))
a_ih✝ : ∀ (a : xr), Subsingleton (Short (xR a))
⊢ Subsingleton (Short (mk xl xr xL xR))
[PROOFSTEP]

| mk xl xr xL xR =>
  constructor
  intro a b
  cases a; cases b
  congr!
    -- Porting note: We use `induction` to prove `subsingleton_short` instead of recursion.
    -- A proof using recursion generates a harder `decreasing_by` goal than in Lean 3 for some reason:
[GOAL]
case mk
xl xr : Type ?u.940
xL : xl → PGame
xR : xr → PGame
a_ih✝¹ : ∀ (a : xl), Subsingleton (Short (xL a))
a_ih✝ : ∀ (a : xr), Subsingleton (Short (xR a))
⊢ Subsingleton (Short (mk xl xr xL xR))
[PROOFSTEP]
constructor
[GOAL]
case mk.allEq
xl xr : Type ?u.940
xL : xl → PGame
xR : xr → PGame
a_ih✝¹ : ∀ (a : xl), Subsingleton (Short (xL a))
a_ih✝ : ∀ (a : xr), Subsingleton (Short (xR a))
⊢ ∀ (a b : Short (mk xl xr xL xR)), a = b
[PROOFSTEP]
intro a b
[GOAL]
case mk.allEq
xl xr : Type ?u.940
xL : xl → PGame
xR : xr → PGame
a_ih✝¹ : ∀ (a : xl), Subsingleton (Short (xL a))
a_ih✝ : ∀ (a : xr), Subsingleton (Short (xR a))
a b : Short (mk xl xr xL xR)
⊢ a = b
[PROOFSTEP]
cases a
[GOAL]
case mk.allEq.mk
xl xr : Type ?u.994
xL : xl → PGame
xR : xr → PGame
a_ih✝¹ : ∀ (a : xl), Subsingleton (Short (xL a))
a_ih✝ : ∀ (a : xr), Subsingleton (Short (xR a))
b : Short (mk xl xr xL xR)
inst✝¹ : Fintype xl
inst✝ : Fintype xr
x✝¹ : (i : xl) → Short (xL i)
x✝ : (j : xr) → Short (xR j)
⊢ Short.mk x✝¹ x✝ = b
[PROOFSTEP]
cases b
[GOAL]
case mk.allEq.mk.mk
xl xr : Type ?u.1179
xL : xl → PGame
xR : xr → PGame
a_ih✝¹ : ∀ (a : xl), Subsingleton (Short (xL a))
a_ih✝ : ∀ (a : xr), Subsingleton (Short (xR a))
inst✝³ : Fintype xl
inst✝² : Fintype xr
x✝³ : (i : xl) → Short (xL i)
x✝² : (j : xr) → Short (xR j)
inst✝¹ : Fintype xl
inst✝ : Fintype xr
x✝¹ : (i : xl) → Short (xL i)
x✝ : (j : xr) → Short (xR j)
⊢ Short.mk x✝³ x✝² = Short.mk x✝¹ x✝
[PROOFSTEP]
congr!
  -- Porting note: We use `induction` to prove `subsingleton_short` instead of recursion.
  -- A proof using recursion generates a harder `decreasing_by` goal than in Lean 3 for some reason:
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
a b : Short (mk xl xr xL xR)
⊢ a = b
[PROOFSTEP]
cases a
[GOAL]
case mk
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
b : Short (mk xl xr xL xR)
inst✝¹ : Fintype xl
inst✝ : Fintype xr
x✝¹ : (i : xl) → Short (xL i)
x✝ : (j : xr) → Short (xR j)
⊢ Short.mk x✝¹ x✝ = b
[PROOFSTEP]
cases b
[GOAL]
case mk.mk
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
inst✝³ : Fintype xl
inst✝² : Fintype xr
x✝³ : (i : xl) → Short (xL i)
x✝² : (j : xr) → Short (xR j)
inst✝¹ : Fintype xl
inst✝ : Fintype xr
x✝¹ : (i : xl) → Short (xL i)
x✝ : (j : xr) → Short (xR j)
⊢ Short.mk x✝³ x✝² = Short.mk x✝¹ x✝
[PROOFSTEP]
congr!
[GOAL]
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) → Short (xL i)
x✝² : (j : xr) → Short (xR j)
inst✝¹ : Fintype xl
inst✝ : Fintype xr
x✝¹ : (i : xl) → Short (xL i)
x✝ : (j : xr) → Short (xR j)
⊢ x✝³ = x✝¹
[PROOFSTEP]
funext x
[GOAL]
case mk.mk.h.e'_5.h
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
inst✝³ : Fintype xl
inst✝² : Fintype xr
x✝³ : (i : xl) → Short (xL i)
x✝² : (j : xr) → Short (xR j)
inst✝¹ : Fintype xl
inst✝ : Fintype xr
x✝¹ : (i : xl) → Short (xL i)
x✝ : (j : xr) → Short (xR j)
x : xl
⊢ x✝³ x = x✝¹ x
[PROOFSTEP]
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.)
[GOAL]
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) → Short (xL i)
x✝² : (j : xr) → Short (xR j)
inst✝¹ : Fintype xl
inst✝ : Fintype xr
x✝¹ : (i : xl) → Short (xL i)
x✝ : (j : xr) → Short (xR j)
⊢ x✝² = x✝
[PROOFSTEP]
funext x
[GOAL]
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) → Short (xL i)
x✝² : (j : xr) → Short (xR j)
inst✝¹ : Fintype xl
inst✝ : Fintype xr
x✝¹ : (i : xl) → Short (xL i)
x✝ : (j : xr) → Short (xR j)
x : xr
⊢ x✝² x = x✝ x
[PROOFSTEP]
apply @Subsingleton.elim _ (subsingleton_short_example (xR x))
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
x✝⁵ : ∀ (y : PGame), (invImage (fun a => a) instWellFoundedRelationPGame).1 y (mk xl xr xL xR) → Subsingleton (Short y)
a b : Short (mk xl xr xL xR)
α β : Type u_1
L : α → PGame
R : β → PGame
x✝⁴ : ∀ (y : PGame), (invImage (fun a => a) instWellFoundedRelationPGame).1 y (mk α β L R) → Subsingleton (Short y)
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) → Short (xL i)
a_eq✝² : HEq xR R✝²
x✝² : (j : xr) → Short (xR j)
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) → Short (xL i)
a_eq✝ : HEq xR R✝
x✝ : (j : xr) → Short (xR j)
h✝ : HEq b (Short.mk x✝¹ x✝)
x : xl
⊢ (invImage (fun a => a) instWellFoundedRelationPGame).1 (xL x) (mk α β L R)
[PROOFSTEP]
{ subst_vars
  simp only [mk.injEq, heq_eq_eq, true_and] at *
  casesm*_ ∧ _
  subst_vars
  pgame_wf_tac
}
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
x✝⁵ : ∀ (y : PGame), (invImage (fun a => a) instWellFoundedRelationPGame).1 y (mk xl xr xL xR) → Subsingleton (Short y)
a b : Short (mk xl xr xL xR)
α β : Type u_1
L : α → PGame
R : β → PGame
x✝⁴ : ∀ (y : PGame), (invImage (fun a => a) instWellFoundedRelationPGame).1 y (mk α β L R) → Subsingleton (Short y)
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) → Short (xL i)
a_eq✝² : HEq xR R✝²
x✝² : (j : xr) → Short (xR j)
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) → Short (xL i)
a_eq✝ : HEq xR R✝
x✝ : (j : xr) → Short (xR j)
h✝ : HEq b (Short.mk x✝¹ x✝)
x : xl
⊢ (invImage (fun a => a) instWellFoundedRelationPGame).1 (xL x) (mk α β L R)
[PROOFSTEP]
subst_vars
[GOAL]
α✝ β✝ : Type u_1
L✝ : α✝ → PGame
R✝ : β✝ → PGame
L xL : α✝ → PGame
inst✝³ : Fintype α✝
x✝⁵ : (i : α✝) → Short (xL i)
inst✝² : Fintype α✝
x✝⁴ : (i : α✝) → Short (xL i)
x : α✝
R xR : β✝ → PGame
inst✝¹ : Fintype β✝
x✝³ : (j : β✝) → Short (xR j)
inst✝ : Fintype β✝
x✝² : (j : β✝) → Short (xR j)
x✝¹ : ∀ (y : PGame), (invImage (fun a => a) instWellFoundedRelationPGame).1 y (mk α✝ β✝ L R) → Subsingleton (Short y)
x✝ : ∀ (y : PGame), (invImage (fun a => a) instWellFoundedRelationPGame).1 y (mk α✝ β✝ xL xR) → Subsingleton (Short y)
h✝¹ : mk α✝ β✝ xL xR = mk α✝ β✝ L R
h✝ : mk α✝ β✝ xL xR = mk α✝ β✝ L✝ R✝
⊢ (invImage (fun a => a) instWellFoundedRelationPGame).1 (xL x) (mk α✝ β✝ L R)
[PROOFSTEP]
simp only [mk.injEq, heq_eq_eq, true_and] at *
[GOAL]
α✝ β✝ : Type u_1
L✝ : α✝ → PGame
R✝ : β✝ → PGame
L xL : α✝ → PGame
inst✝³ : Fintype α✝
x✝⁵ : (i : α✝) → Short (xL i)
inst✝² : Fintype α✝
x✝⁴ : (i : α✝) → Short (xL i)
x : α✝
R xR : β✝ → PGame
inst✝¹ : Fintype β✝
x✝³ : (j : β✝) → Short (xR j)
inst✝ : Fintype β✝
x✝² : (j : β✝) → Short (xR j)
x✝¹ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun a => a) y (mk α✝ β✝ L R) → Subsingleton (Short y)
x✝ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun a => a) y (mk α✝ β✝ xL xR) → Subsingleton (Short y)
h✝¹ : xL = L ∧ xR = R
h✝ : xL = L✝ ∧ xR = R✝
⊢ InvImage WellFoundedRelation.rel (fun a => a) (xL x) (mk α✝ β✝ L R)
[PROOFSTEP]
casesm*_ ∧ _
[GOAL]
case intro.intro
α✝ β✝ : Type u_1
L✝ : α✝ → PGame
R✝ : β✝ → PGame
L xL : α✝ → PGame
inst✝³ : Fintype α✝
x✝⁵ : (i : α✝) → Short (xL i)
inst✝² : Fintype α✝
x✝⁴ : (i : α✝) → Short (xL i)
x : α✝
R xR : β✝ → PGame
inst✝¹ : Fintype β✝
x✝³ : (j : β✝) → Short (xR j)
inst✝ : Fintype β✝
x✝² : (j : β✝) → Short (xR j)
x✝¹ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun a => a) y (mk α✝ β✝ L R) → Subsingleton (Short y)
x✝ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun a => a) y (mk α✝ β✝ xL xR) → Subsingleton (Short y)
left✝¹ : xL = L
right✝¹ : xR = R
left✝ : xL = L✝
right✝ : xR = R✝
⊢ InvImage WellFoundedRelation.rel (fun a => a) (xL x) (mk α✝ β✝ L R)
[PROOFSTEP]
subst_vars
[GOAL]
case intro.intro
α✝ β✝ : Type u_1
xL : α✝ → PGame
inst✝³ : Fintype α✝
x✝⁵ : (i : α✝) → Short (xL i)
inst✝² : Fintype α✝
x✝⁴ : (i : α✝) → Short (xL i)
x : α✝
xR : β✝ → PGame
inst✝¹ : Fintype β✝
x✝³ : (j : β✝) → Short (xR j)
inst✝ : Fintype β✝
x✝² : (j : β✝) → Short (xR j)
x✝¹ x✝ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun a => a) y (mk α✝ β✝ xL xR) → Subsingleton (Short y)
⊢ InvImage WellFoundedRelation.rel (fun a => a) (xL x) (mk α✝ β✝ xL xR)
[PROOFSTEP]
pgame_wf_tac
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
x✝⁵ : ∀ (y : PGame), (invImage (fun a => a) instWellFoundedRelationPGame).1 y (mk xl xr xL xR) → Subsingleton (Short y)
a b : Short (mk xl xr xL xR)
α β : Type u_1
L : α → PGame
R : β → PGame
x✝⁴ : ∀ (y : PGame), (invImage (fun a => a) instWellFoundedRelationPGame).1 y (mk α β L R) → Subsingleton (Short y)
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) → Short (xL i)
a_eq✝² : HEq xR R✝²
x✝² : (j : xr) → Short (xR j)
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) → Short (xL i)
a_eq✝ : HEq xR R✝
x✝ : (j : xr) → Short (xR j)
h✝ : HEq b (Short.mk x✝¹ x✝)
x : xr
⊢ (invImage (fun a => a) instWellFoundedRelationPGame).1 (xR x) (mk α β L R)
[PROOFSTEP]
{ subst_vars
  simp only [mk.injEq, heq_eq_eq, true_and] at *
  casesm*_ ∧ _
  subst_vars
  pgame_wf_tac
}
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
x✝⁵ : ∀ (y : PGame), (invImage (fun a => a) instWellFoundedRelationPGame).1 y (mk xl xr xL xR) → Subsingleton (Short y)
a b : Short (mk xl xr xL xR)
α β : Type u_1
L : α → PGame
R : β → PGame
x✝⁴ : ∀ (y : PGame), (invImage (fun a => a) instWellFoundedRelationPGame).1 y (mk α β L R) → Subsingleton (Short y)
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) → Short (xL i)
a_eq✝² : HEq xR R✝²
x✝² : (j : xr) → Short (xR j)
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) → Short (xL i)
a_eq✝ : HEq xR R✝
x✝ : (j : xr) → Short (xR j)
h✝ : HEq b (Short.mk x✝¹ x✝)
x : xr
⊢ (invImage (fun a => a) instWellFoundedRelationPGame).1 (xR x) (mk α β L R)
[PROOFSTEP]
subst_vars
[GOAL]
α✝ β✝ : Type u_1
L✝ : α✝ → PGame
R✝ : β✝ → PGame
L xL : α✝ → PGame
inst✝³ : Fintype α✝
x✝⁵ : (i : α✝) → Short (xL i)
inst✝² : Fintype α✝
x✝⁴ : (i : α✝) → Short (xL i)
R xR : β✝ → PGame
inst✝¹ : Fintype β✝
x✝³ : (j : β✝) → Short (xR j)
inst✝ : Fintype β✝
x✝² : (j : β✝) → Short (xR j)
x : β✝
x✝¹ : ∀ (y : PGame), (invImage (fun a => a) instWellFoundedRelationPGame).1 y (mk α✝ β✝ L R) → Subsingleton (Short y)
x✝ : ∀ (y : PGame), (invImage (fun a => a) instWellFoundedRelationPGame).1 y (mk α✝ β✝ xL xR) → Subsingleton (Short y)
h✝¹ : mk α✝ β✝ xL xR = mk α✝ β✝ L R
h✝ : mk α✝ β✝ xL xR = mk α✝ β✝ L✝ R✝
⊢ (invImage (fun a => a) instWellFoundedRelationPGame).1 (xR x) (mk α✝ β✝ L R)
[PROOFSTEP]
simp only [mk.injEq, heq_eq_eq, true_and] at *
[GOAL]
α✝ β✝ : Type u_1
L✝ : α✝ → PGame
R✝ : β✝ → PGame
L xL : α✝ → PGame
inst✝³ : Fintype α✝
x✝⁵ : (i : α✝) → Short (xL i)
inst✝² : Fintype α✝
x✝⁴ : (i : α✝) → Short (xL i)
R xR : β✝ → PGame
inst✝¹ : Fintype β✝
x✝³ : (j : β✝) → Short (xR j)
inst✝ : Fintype β✝
x✝² : (j : β✝) → Short (xR j)
x : β✝
x✝¹ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun a => a) y (mk α✝ β✝ L R) → Subsingleton (Short y)
x✝ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun a => a) y (mk α✝ β✝ xL xR) → Subsingleton (Short y)
h✝¹ : xL = L ∧ xR = R
h✝ : xL = L✝ ∧ xR = R✝
⊢ InvImage WellFoundedRelation.rel (fun a => a) (xR x) (mk α✝ β✝ L R)
[PROOFSTEP]
casesm*_ ∧ _
[GOAL]
case intro.intro
α✝ β✝ : Type u_1
L✝ : α✝ → PGame
R✝ : β✝ → PGame
L xL : α✝ → PGame
inst✝³ : Fintype α✝
x✝⁵ : (i : α✝) → Short (xL i)
inst✝² : Fintype α✝
x✝⁴ : (i : α✝) → Short (xL i)
R xR : β✝ → PGame
inst✝¹ : Fintype β✝
x✝³ : (j : β✝) → Short (xR j)
inst✝ : Fintype β✝
x✝² : (j : β✝) → Short (xR j)
x : β✝
x✝¹ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun a => a) y (mk α✝ β✝ L R) → Subsingleton (Short y)
x✝ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun a => a) y (mk α✝ β✝ xL xR) → Subsingleton (Short y)
left✝¹ : xL = L
right✝¹ : xR = R
left✝ : xL = L✝
right✝ : xR = R✝
⊢ InvImage WellFoundedRelation.rel (fun a => a) (xR x) (mk α✝ β✝ L R)
[PROOFSTEP]
subst_vars
[GOAL]
case intro.intro
α✝ β✝ : Type u_1
xL : α✝ → PGame
inst✝³ : Fintype α✝
x✝⁵ : (i : α✝) → Short (xL i)
inst✝² : Fintype α✝
x✝⁴ : (i : α✝) → Short (xL i)
xR : β✝ → PGame
inst✝¹ : Fintype β✝
x✝³ : (j : β✝) → Short (xR j)
inst✝ : Fintype β✝
x✝² : (j : β✝) → Short (xR j)
x : β✝
x✝¹ x✝ : ∀ (y : PGame), InvImage WellFoundedRelation.rel (fun a => a) y (mk α✝ β✝ xL xR) → Subsingleton (Short y)
⊢ InvImage WellFoundedRelation.rel (fun a => a) (xR x) (mk α✝ β✝ xL xR)
[PROOFSTEP]
pgame_wf_tac
[GOAL]
x : PGame
inst✝¹ : Fintype (LeftMoves x)
inst✝ : Fintype (RightMoves x)
sL : (i : LeftMoves x) → Short (moveLeft x i)
sR : (j : RightMoves x) → Short (moveRight x j)
⊢ Short x
[PROOFSTEP]
convert Short.mk sL sR
[GOAL]
case h.e'_1
x : PGame
inst✝¹ : Fintype (LeftMoves x)
inst✝ : Fintype (RightMoves x)
sL : (i : LeftMoves x) → Short (moveLeft x i)
sR : (j : RightMoves x) → Short (moveRight x j)
⊢ x = PGame.mk (LeftMoves x) (RightMoves x) (fun i => moveLeft x i) fun j => moveRight x j
[PROOFSTEP]
cases x
[GOAL]
case h.e'_1.mk
α✝ β✝ : Type ?u.18601
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
inst✝¹ : Fintype (LeftMoves (PGame.mk α✝ β✝ a✝¹ a✝))
inst✝ : Fintype (RightMoves (PGame.mk α✝ β✝ a✝¹ a✝))
sL : (i : LeftMoves (PGame.mk α✝ β✝ a✝¹ a✝)) → Short (moveLeft (PGame.mk α✝ β✝ a✝¹ a✝) i)
sR : (j : RightMoves (PGame.mk α✝ β✝ a✝¹ a✝)) → Short (moveRight (PGame.mk α✝ β✝ a✝¹ a✝) j)
⊢ PGame.mk α✝ β✝ a✝¹ a✝ =
    PGame.mk (LeftMoves (PGame.mk α✝ β✝ a✝¹ a✝)) (RightMoves (PGame.mk α✝ β✝ a✝¹ a✝))
      (fun i => moveLeft (PGame.mk α✝ β✝ a✝¹ a✝) i) fun j => moveRight (PGame.mk α✝ β✝ a✝¹ a✝) j
[PROOFSTEP]
dsimp
[GOAL]
α β : Type u
L : α → PGame
R : β → PGame
S : Short (mk α β L R)
⊢ Fintype α
[PROOFSTEP]
cases' S with _ _ _ _ _ _ F _
[GOAL]
case mk
α β : Type u
L : α → PGame
R : β → PGame
F : Fintype α
inst✝ : Fintype β
x✝¹ : (i : α) → Short (L i)
x✝ : (j : β) → Short (R j)
⊢ Fintype α
[PROOFSTEP]
exact F
[GOAL]
x : PGame
S : Short x
⊢ Fintype (LeftMoves x)
[PROOFSTEP]
cases S
[GOAL]
case mk
α✝ β✝ : Type ?u.19495
L✝ : α✝ → PGame
R✝ : β✝ → PGame
x✝¹ : (i : α✝) → Short (L✝ i)
x✝ : (j : β✝) → Short (R✝ j)
inst✝¹ : Fintype α✝
inst✝ : Fintype β✝
⊢ Fintype (LeftMoves (mk α✝ β✝ L✝ R✝))
[PROOFSTEP]
assumption
[GOAL]
α β : Type u
L : α → PGame
R : β → PGame
S : Short (mk α β L R)
⊢ Fintype β
[PROOFSTEP]
cases' S with _ _ _ _ _ _ _ F
[GOAL]
case mk
α β : Type u
L : α → PGame
R : β → PGame
inst✝ : Fintype α
F : Fintype β
x✝¹ : (i : α) → Short (L i)
x✝ : (j : β) → Short (R j)
⊢ Fintype β
[PROOFSTEP]
exact F
[GOAL]
x : PGame
S : Short x
⊢ Fintype (RightMoves x)
[PROOFSTEP]
cases S
[GOAL]
case mk
α✝ β✝ : Type ?u.20394
L✝ : α✝ → PGame
R✝ : β✝ → PGame
x✝¹ : (i : α✝) → Short (L✝ i)
x✝ : (j : β✝) → Short (R✝ j)
inst✝¹ : Fintype α✝
inst✝ : Fintype β✝
⊢ Fintype (RightMoves (mk α✝ β✝ L✝ R✝))
[PROOFSTEP]
assumption
[GOAL]
x : PGame
S : Short x
i : LeftMoves x
⊢ Short (moveLeft x i)
[PROOFSTEP]
cases' S with _ _ _ _ L _ _ _
[GOAL]
case mk
α✝ β✝ : Type ?u.20673
L✝ : α✝ → PGame
R✝ : β✝ → PGame
L : (i : α✝) → Short (L✝ i)
x✝ : (j : β✝) → Short (R✝ j)
inst✝¹ : Fintype α✝
inst✝ : Fintype β✝
i : LeftMoves (mk α✝ β✝ L✝ R✝)
⊢ Short (moveLeft (mk α✝ β✝ L✝ R✝) i)
[PROOFSTEP]
apply L
[GOAL]
xl xr : Type ?u.20966
xL : xl → PGame
xR : xr → PGame
S : Short (mk xl xr xL xR)
i : xl
⊢ Short (xL i)
[PROOFSTEP]
cases' S with _ _ _ _ L _ _ _
[GOAL]
case mk
xl xr : Type ?u.21003
xL : xl → PGame
xR : xr → PGame
i : xl
inst✝¹ : Fintype xl
inst✝ : Fintype xr
L : (i : xl) → Short (xL i)
x✝ : (j : xr) → Short (xR j)
⊢ Short (xL i)
[PROOFSTEP]
apply L
[GOAL]
x : PGame
S : Short x
j : RightMoves x
⊢ Short (moveRight x j)
[PROOFSTEP]
cases' S with _ _ _ _ _ R _ _
[GOAL]
case mk
α✝ β✝ : Type ?u.21648
L✝ : α✝ → PGame
R✝ : β✝ → PGame
x✝ : (i : α✝) → Short (L✝ i)
R : (j : β✝) → Short (R✝ j)
inst✝¹ : Fintype α✝
inst✝ : Fintype β✝
j : RightMoves (mk α✝ β✝ L✝ R✝)
⊢ Short (moveRight (mk α✝ β✝ L✝ R✝) j)
[PROOFSTEP]
apply R
[GOAL]
xl xr : Type ?u.21941
xL : xl → PGame
xR : xr → PGame
S : Short (mk xl xr xL xR)
j : xr
⊢ Short (xR j)
[PROOFSTEP]
cases' S with _ _ _ _ _ R _ _
[GOAL]
case mk
xl xr : Type ?u.21978
xL : xl → PGame
xR : xr → PGame
j : xr
inst✝¹ : Fintype xl
inst✝ : Fintype xr
x✝ : (i : xl) → Short (xL i)
R : (j : xr) → Short (xR j)
⊢ Short (xR j)
[PROOFSTEP]
apply R
[GOAL]
x : PGame
⊢ ∀ [inst : Short x], birthday x < Ordinal.omega
[PROOFSTEP]
induction x with
| mk xl xr xL xR ihl ihr =>
  intro hs
  rcases hs with ⟨sL, sR⟩
  rw [birthday, max_lt_iff]
  constructor
  all_goals
    rw [← Cardinal.ord_aleph0]
    refine'
      Cardinal.lsub_lt_ord_of_isRegular.{u, u} Cardinal.isRegular_aleph0 (Cardinal.lt_aleph0_of_finite _) fun i => _
    rw [Cardinal.ord_aleph0]
  · apply ihl
  · apply ihr
[GOAL]
x : PGame
⊢ ∀ [inst : Short x], birthday x < Ordinal.omega
[PROOFSTEP]
induction x with
| mk xl xr xL xR ihl ihr =>
  intro hs
  rcases hs with ⟨sL, sR⟩
  rw [birthday, max_lt_iff]
  constructor
  all_goals
    rw [← Cardinal.ord_aleph0]
    refine'
      Cardinal.lsub_lt_ord_of_isRegular.{u, u} Cardinal.isRegular_aleph0 (Cardinal.lt_aleph0_of_finite _) fun i => _
    rw [Cardinal.ord_aleph0]
  · apply ihl
  · apply ihr
[GOAL]
case mk
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
⊢ ∀ [inst : Short (mk xl xr xL xR)], birthday (mk xl xr xL xR) < Ordinal.omega
[PROOFSTEP]

| mk xl xr xL xR ihl ihr =>
  intro hs
  rcases hs with ⟨sL, sR⟩
  rw [birthday, max_lt_iff]
  constructor
  all_goals
    rw [← Cardinal.ord_aleph0]
    refine'
      Cardinal.lsub_lt_ord_of_isRegular.{u, u} Cardinal.isRegular_aleph0 (Cardinal.lt_aleph0_of_finite _) fun i => _
    rw [Cardinal.ord_aleph0]
  · apply ihl
  · apply ihr
[GOAL]
case mk
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
⊢ ∀ [inst : Short (mk xl xr xL xR)], birthday (mk xl xr xL xR) < Ordinal.omega
[PROOFSTEP]
intro hs
[GOAL]
case mk
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
hs : Short (mk xl xr xL xR)
⊢ birthday (mk xl xr xL xR) < Ordinal.omega
[PROOFSTEP]
rcases hs with ⟨sL, sR⟩
[GOAL]
case mk.mk
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → Short (xL i)
sR : (j : xr) → Short (xR j)
⊢ birthday (mk xl xr xL xR) < Ordinal.omega
[PROOFSTEP]
rw [birthday, max_lt_iff]
[GOAL]
case mk.mk
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → Short (xL i)
sR : (j : xr) → Short (xR j)
⊢ (Ordinal.lsub fun i => birthday (xL i)) < Ordinal.omega ∧ (Ordinal.lsub fun i => birthday (xR i)) < Ordinal.omega
[PROOFSTEP]
constructor
[GOAL]
case mk.mk.left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → Short (xL i)
sR : (j : xr) → Short (xR j)
⊢ (Ordinal.lsub fun i => birthday (xL i)) < Ordinal.omega
case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → Short (xL i)
sR : (j : xr) → Short (xR j)
⊢ (Ordinal.lsub fun i => birthday (xR i)) < Ordinal.omega
[PROOFSTEP]
all_goals
  rw [← Cardinal.ord_aleph0]
  refine' Cardinal.lsub_lt_ord_of_isRegular.{u, u} Cardinal.isRegular_aleph0 (Cardinal.lt_aleph0_of_finite _) fun i => _
  rw [Cardinal.ord_aleph0]
[GOAL]
case mk.mk.left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → Short (xL i)
sR : (j : xr) → Short (xR j)
⊢ (Ordinal.lsub fun i => birthday (xL i)) < Ordinal.omega
[PROOFSTEP]
rw [← Cardinal.ord_aleph0]
[GOAL]
case mk.mk.left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → Short (xL i)
sR : (j : xr) → Short (xR j)
⊢ (Ordinal.lsub fun i => birthday (xL i)) < Cardinal.ord Cardinal.aleph0
[PROOFSTEP]
refine' Cardinal.lsub_lt_ord_of_isRegular.{u, u} Cardinal.isRegular_aleph0 (Cardinal.lt_aleph0_of_finite _) fun i => _
[GOAL]
case mk.mk.left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → Short (xL i)
sR : (j : xr) → Short (xR j)
i : xl
⊢ birthday (xL i) < Cardinal.ord Cardinal.aleph0
[PROOFSTEP]
rw [Cardinal.ord_aleph0]
[GOAL]
case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → Short (xL i)
sR : (j : xr) → Short (xR j)
⊢ (Ordinal.lsub fun i => birthday (xR i)) < Ordinal.omega
[PROOFSTEP]
rw [← Cardinal.ord_aleph0]
[GOAL]
case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → Short (xL i)
sR : (j : xr) → Short (xR j)
⊢ (Ordinal.lsub fun i => birthday (xR i)) < Cardinal.ord Cardinal.aleph0
[PROOFSTEP]
refine' Cardinal.lsub_lt_ord_of_isRegular.{u, u} Cardinal.isRegular_aleph0 (Cardinal.lt_aleph0_of_finite _) fun i => _
[GOAL]
case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → Short (xL i)
sR : (j : xr) → Short (xR j)
i : xr
⊢ birthday (xR i) < Cardinal.ord Cardinal.aleph0
[PROOFSTEP]
rw [Cardinal.ord_aleph0]
[GOAL]
case mk.mk.left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → Short (xL i)
sR : (j : xr) → Short (xR j)
i : xl
⊢ birthday (xL i) < Ordinal.omega
[PROOFSTEP]
apply ihl
[GOAL]
case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : Short (xL a)], birthday (xL a) < Ordinal.omega
ihr : ∀ (a : xr) [inst : Short (xR a)], birthday (xR a) < Ordinal.omega
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → Short (xL i)
sR : (j : xr) → Short (xR j)
i : xr
⊢ birthday (xR i) < Ordinal.omega
[PROOFSTEP]
apply ihr
[GOAL]
i : PUnit
⊢ Short 0
[PROOFSTEP]
cases i
[GOAL]
case unit
⊢ Short 0
[PROOFSTEP]
infer_instance
[GOAL]
j : PEmpty
⊢ Short (PEmpty.elim j)
[PROOFSTEP]
cases j
[GOAL]
x✝ : ListShort []
n : Fin (List.length [])
⊢ Short (List.get [] n)
[PROOFSTEP]
exfalso
[GOAL]
case h
x✝ : ListShort []
n : Fin (List.length [])
⊢ False
[PROOFSTEP]
rcases n with
  ⟨_, ⟨⟩⟩
    -- Porting note: The proof errors unless `done` or a `;` is added after `rcases`
[GOAL]

[PROOFSTEP]
done
[GOAL]
L : List PGame
inst✝ : ListShort L
i : Fin (List.length L)
⊢ Short (List.nthLe L ↑i (_ : ↑i < List.length L))
[PROOFSTEP]
rw [List.nthLe_eq]
[GOAL]
L : List PGame
inst✝ : ListShort L
i : Fin (List.length L)
⊢ Short (List.get L { val := ↑i, isLt := (_ : ↑i < List.length L) })
[PROOFSTEP]
apply listShortGet
[GOAL]
L R : List PGame
x✝¹ : ListShort L
x✝ : ListShort R
⊢ Short (ofLists L R)
[PROOFSTEP]
apply Short.mk
[GOAL]
case x
L R : List PGame
x✝¹ : ListShort L
x✝ : ListShort R
⊢ (i : ULift (Fin (List.length L))) → Short (List.nthLe L ↑i.down (_ : ↑i.down < List.length L))
[PROOFSTEP]
intros
[GOAL]
case x
L R : List PGame
x✝¹ : ListShort L
x✝ : ListShort R
i✝ : ULift (Fin (List.length L))
⊢ Short (List.nthLe L ↑i✝.down (_ : ↑i✝.down < List.length L))
[PROOFSTEP]
infer_instance
[GOAL]
case x
L R : List PGame
x✝¹ : ListShort L
x✝ : ListShort R
⊢ (j : ULift (Fin (List.length R))) → Short (List.nthLe R ↑j.down (_ : ↑j.down < List.length R))
[PROOFSTEP]
intros
[GOAL]
case x
L R : List PGame
x✝¹ : ListShort L
x✝ : ListShort R
j✝ : ULift (Fin (List.length R))
⊢ Short (List.nthLe R ↑j✝.down (_ : ↑j✝.down < List.length R))
[PROOFSTEP]
apply PGame.listShortGet
[GOAL]
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
rL : (i : LeftMoves x) → moveLeft x i ≡r moveLeft y (↑L i)
rR : (j : RightMoves x) → moveRight x j ≡r moveRight y (↑R j)
S : Short x
⊢ Short y
[PROOFSTEP]
haveI := Fintype.ofEquiv _ L
[GOAL]
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
rL : (i : LeftMoves x) → moveLeft x i ≡r moveLeft y (↑L i)
rR : (j : RightMoves x) → moveRight x j ≡r moveRight y (↑R j)
S : Short x
this : Fintype (LeftMoves y)
⊢ Short y
[PROOFSTEP]
haveI := Fintype.ofEquiv _ R
[GOAL]
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
rL : (i : LeftMoves x) → moveLeft x i ≡r moveLeft y (↑L i)
rR : (j : RightMoves x) → moveRight x j ≡r moveRight y (↑R j)
S : Short x
this✝ : Fintype (LeftMoves y)
this : Fintype (RightMoves y)
⊢ Short y
[PROOFSTEP]
exact
  Short.mk' (fun i => by rw [← L.right_inv i]; apply shortOfRelabelling (rL (L.symm i)) inferInstance) fun j => by
    simpa using shortOfRelabelling (rR (R.symm j)) inferInstance
[GOAL]
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
rL : (i : LeftMoves x) → moveLeft x i ≡r moveLeft y (↑L i)
rR : (j : RightMoves x) → moveRight x j ≡r moveRight y (↑R j)
S : Short x
this✝ : Fintype (LeftMoves y)
this : Fintype (RightMoves y)
i : LeftMoves y
⊢ Short (moveLeft y i)
[PROOFSTEP]
rw [← L.right_inv i]
[GOAL]
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
rL : (i : LeftMoves x) → moveLeft x i ≡r moveLeft y (↑L i)
rR : (j : RightMoves x) → moveRight x j ≡r moveRight y (↑R j)
S : Short x
this✝ : Fintype (LeftMoves y)
this : Fintype (RightMoves y)
i : LeftMoves y
⊢ Short (moveLeft y (Equiv.toFun L (Equiv.invFun L i)))
[PROOFSTEP]
apply shortOfRelabelling (rL (L.symm i)) inferInstance
[GOAL]
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
rL : (i : LeftMoves x) → moveLeft x i ≡r moveLeft y (↑L i)
rR : (j : RightMoves x) → moveRight x j ≡r moveRight y (↑R j)
S : Short x
this✝ : Fintype (LeftMoves y)
this : Fintype (RightMoves y)
j : RightMoves y
⊢ Short (moveRight y j)
[PROOFSTEP]
simpa using shortOfRelabelling (rR (R.symm j)) inferInstance
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
x✝ : Short (mk xl xr xL xR)
⊢ Short (-mk xl xr xL xR)
[PROOFSTEP]
exact
  Short.mk (fun i => shortNeg _) fun i =>
    shortNeg
      _
        -- Porting note: `decreasing_by pgame_wf_tac` is no longer needed.
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
x✝¹ : Short (mk xl xr xL xR)
x✝ : Short (mk yl yr yL yR)
⊢ Short (mk xl xr xL xR + mk yl yr yL yR)
[PROOFSTEP]
apply Short.mk
[GOAL]
case x
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
x✝¹ : Short (mk xl xr xL xR)
x✝ : Short (mk yl yr yL yR)
⊢ (i : xl ⊕ yl) →
    Short
      (Sum.rec
        (fun i =>
          (fun a =>
              rec (motive := fun x => PGame → PGame)
                (fun xl xr a a IHxl IHxr y =>
                  rec
                    (fun yl yr yL yR IHyl IHyr =>
                      let_fun y := mk yl yr yL yR;
                      mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                        Sum.rec (fun i => IHxr i y) IHyr t)
                    y)
                (xL a))
            i (mk yl yr yL yR))
        (fun a =>
          rec
            (fun yl yr yL yR IHyl IHyr =>
              let_fun y := mk yl yr yL yR;
              mk (xl ⊕ yl) (xr ⊕ yr)
                (fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := mk yl yr yL yR;
                                  mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xL a))
                        i y)
                    IHyl t)
                fun t =>
                Sum.rec
                  (fun i =>
                    (fun a =>
                        rec (motive := fun x => PGame → PGame)
                          (fun xl xr a a IHxl IHxr y =>
                            rec
                              (fun yl yr yL yR IHyl IHyr =>
                                let_fun y := mk yl yr yL yR;
                                mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                  Sum.rec (fun i => IHxr i y) IHyr t)
                              y)
                          (xR a))
                      i y)
                  IHyr t)
            (yL a))
        i)
case x
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
x✝¹ : Short (mk xl xr xL xR)
x✝ : Short (mk yl yr yL yR)
⊢ (j : xr ⊕ yr) →
    Short
      (Sum.rec
        (fun i =>
          (fun a =>
              rec (motive := fun x => PGame → PGame)
                (fun xl xr a a IHxl IHxr y =>
                  rec
                    (fun yl yr yL yR IHyl IHyr =>
                      let_fun y := mk yl yr yL yR;
                      mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                        Sum.rec (fun i => IHxr i y) IHyr t)
                    y)
                (xR a))
            i (mk yl yr yL yR))
        (fun a =>
          rec
            (fun yl yr yL yR IHyl IHyr =>
              let_fun y := mk yl yr yL yR;
              mk (xl ⊕ yl) (xr ⊕ yr)
                (fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := mk yl yr yL yR;
                                  mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xL a))
                        i y)
                    IHyl t)
                fun t =>
                Sum.rec
                  (fun i =>
                    (fun a =>
                        rec (motive := fun x => PGame → PGame)
                          (fun xl xr a a IHxl IHxr y =>
                            rec
                              (fun yl yr yL yR IHyl IHyr =>
                                let_fun y := mk yl yr yL yR;
                                mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                  Sum.rec (fun i => IHxr i y) IHyr t)
                              y)
                          (xR a))
                      i y)
                  IHyr t)
            (yR a))
        j)
[PROOFSTEP]
all_goals
  rintro ⟨i⟩
  · apply shortAdd
  · change Short (mk xl xr xL xR + _); apply shortAdd
[GOAL]
case x
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
x✝¹ : Short (mk xl xr xL xR)
x✝ : Short (mk yl yr yL yR)
⊢ (i : xl ⊕ yl) →
    Short
      (Sum.rec
        (fun i =>
          (fun a =>
              rec (motive := fun x => PGame → PGame)
                (fun xl xr a a IHxl IHxr y =>
                  rec
                    (fun yl yr yL yR IHyl IHyr =>
                      let_fun y := mk yl yr yL yR;
                      mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                        Sum.rec (fun i => IHxr i y) IHyr t)
                    y)
                (xL a))
            i (mk yl yr yL yR))
        (fun a =>
          rec
            (fun yl yr yL yR IHyl IHyr =>
              let_fun y := mk yl yr yL yR;
              mk (xl ⊕ yl) (xr ⊕ yr)
                (fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := mk yl yr yL yR;
                                  mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xL a))
                        i y)
                    IHyl t)
                fun t =>
                Sum.rec
                  (fun i =>
                    (fun a =>
                        rec (motive := fun x => PGame → PGame)
                          (fun xl xr a a IHxl IHxr y =>
                            rec
                              (fun yl yr yL yR IHyl IHyr =>
                                let_fun y := mk yl yr yL yR;
                                mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                  Sum.rec (fun i => IHxr i y) IHyr t)
                              y)
                          (xR a))
                      i y)
                  IHyr t)
            (yL a))
        i)
[PROOFSTEP]
rintro ⟨i⟩
[GOAL]
case x.inl
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
x✝¹ : Short (mk xl xr xL xR)
x✝ : Short (mk yl yr yL yR)
i : xl
⊢ Short
    (Sum.rec
      (fun i =>
        (fun a =>
            rec (motive := fun x => PGame → PGame)
              (fun xl xr a a IHxl IHxr y =>
                rec
                  (fun yl yr yL yR IHyl IHyr =>
                    let_fun y := mk yl yr yL yR;
                    mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                      Sum.rec (fun i => IHxr i y) IHyr t)
                  y)
              (xL a))
          i (mk yl yr yL yR))
      (fun a =>
        rec
          (fun yl yr yL yR IHyl IHyr =>
            let_fun y := mk yl yr yL yR;
            mk (xl ⊕ yl) (xr ⊕ yr)
              (fun t =>
                Sum.rec
                  (fun i =>
                    (fun a =>
                        rec (motive := fun x => PGame → PGame)
                          (fun xl xr a a IHxl IHxr y =>
                            rec
                              (fun yl yr yL yR IHyl IHyr =>
                                let_fun y := mk yl yr yL yR;
                                mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                  Sum.rec (fun i => IHxr i y) IHyr t)
                              y)
                          (xL a))
                      i y)
                  IHyl t)
              fun t =>
              Sum.rec
                (fun i =>
                  (fun a =>
                      rec (motive := fun x => PGame → PGame)
                        (fun xl xr a a IHxl IHxr y =>
                          rec
                            (fun yl yr yL yR IHyl IHyr =>
                              let_fun y := mk yl yr yL yR;
                              mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                Sum.rec (fun i => IHxr i y) IHyr t)
                            y)
                        (xR a))
                    i y)
                IHyr t)
          (yL a))
      (Sum.inl i))
[PROOFSTEP]
apply shortAdd
[GOAL]
case x.inr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
x✝¹ : Short (mk xl xr xL xR)
x✝ : Short (mk yl yr yL yR)
val✝ : yl
⊢ Short
    (Sum.rec
      (fun i =>
        (fun a =>
            rec (motive := fun x => PGame → PGame)
              (fun xl xr a a IHxl IHxr y =>
                rec
                  (fun yl yr yL yR IHyl IHyr =>
                    let_fun y := mk yl yr yL yR;
                    mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                      Sum.rec (fun i => IHxr i y) IHyr t)
                  y)
              (xL a))
          i (mk yl yr yL yR))
      (fun a =>
        rec
          (fun yl yr yL yR IHyl IHyr =>
            let_fun y := mk yl yr yL yR;
            mk (xl ⊕ yl) (xr ⊕ yr)
              (fun t =>
                Sum.rec
                  (fun i =>
                    (fun a =>
                        rec (motive := fun x => PGame → PGame)
                          (fun xl xr a a IHxl IHxr y =>
                            rec
                              (fun yl yr yL yR IHyl IHyr =>
                                let_fun y := mk yl yr yL yR;
                                mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                  Sum.rec (fun i => IHxr i y) IHyr t)
                              y)
                          (xL a))
                      i y)
                  IHyl t)
              fun t =>
              Sum.rec
                (fun i =>
                  (fun a =>
                      rec (motive := fun x => PGame → PGame)
                        (fun xl xr a a IHxl IHxr y =>
                          rec
                            (fun yl yr yL yR IHyl IHyr =>
                              let_fun y := mk yl yr yL yR;
                              mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                Sum.rec (fun i => IHxr i y) IHyr t)
                            y)
                        (xR a))
                    i y)
                IHyr t)
          (yL a))
      (Sum.inr val✝))
[PROOFSTEP]
change Short (mk xl xr xL xR + _)
[GOAL]
case x.inr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
x✝¹ : Short (mk xl xr xL xR)
x✝ : Short (mk yl yr yL yR)
val✝ : yl
⊢ Short (mk xl xr xL xR + yL val✝)
[PROOFSTEP]
apply shortAdd
[GOAL]
case x
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
x✝¹ : Short (mk xl xr xL xR)
x✝ : Short (mk yl yr yL yR)
⊢ (j : xr ⊕ yr) →
    Short
      (Sum.rec
        (fun i =>
          (fun a =>
              rec (motive := fun x => PGame → PGame)
                (fun xl xr a a IHxl IHxr y =>
                  rec
                    (fun yl yr yL yR IHyl IHyr =>
                      let_fun y := mk yl yr yL yR;
                      mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                        Sum.rec (fun i => IHxr i y) IHyr t)
                    y)
                (xR a))
            i (mk yl yr yL yR))
        (fun a =>
          rec
            (fun yl yr yL yR IHyl IHyr =>
              let_fun y := mk yl yr yL yR;
              mk (xl ⊕ yl) (xr ⊕ yr)
                (fun t =>
                  Sum.rec
                    (fun i =>
                      (fun a =>
                          rec (motive := fun x => PGame → PGame)
                            (fun xl xr a a IHxl IHxr y =>
                              rec
                                (fun yl yr yL yR IHyl IHyr =>
                                  let_fun y := mk yl yr yL yR;
                                  mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                    Sum.rec (fun i => IHxr i y) IHyr t)
                                y)
                            (xL a))
                        i y)
                    IHyl t)
                fun t =>
                Sum.rec
                  (fun i =>
                    (fun a =>
                        rec (motive := fun x => PGame → PGame)
                          (fun xl xr a a IHxl IHxr y =>
                            rec
                              (fun yl yr yL yR IHyl IHyr =>
                                let_fun y := mk yl yr yL yR;
                                mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                  Sum.rec (fun i => IHxr i y) IHyr t)
                              y)
                          (xR a))
                      i y)
                  IHyr t)
            (yR a))
        j)
[PROOFSTEP]
rintro ⟨i⟩
[GOAL]
case x.inl
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
x✝¹ : Short (mk xl xr xL xR)
x✝ : Short (mk yl yr yL yR)
i : xr
⊢ Short
    (Sum.rec
      (fun i =>
        (fun a =>
            rec (motive := fun x => PGame → PGame)
              (fun xl xr a a IHxl IHxr y =>
                rec
                  (fun yl yr yL yR IHyl IHyr =>
                    let_fun y := mk yl yr yL yR;
                    mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                      Sum.rec (fun i => IHxr i y) IHyr t)
                  y)
              (xR a))
          i (mk yl yr yL yR))
      (fun a =>
        rec
          (fun yl yr yL yR IHyl IHyr =>
            let_fun y := mk yl yr yL yR;
            mk (xl ⊕ yl) (xr ⊕ yr)
              (fun t =>
                Sum.rec
                  (fun i =>
                    (fun a =>
                        rec (motive := fun x => PGame → PGame)
                          (fun xl xr a a IHxl IHxr y =>
                            rec
                              (fun yl yr yL yR IHyl IHyr =>
                                let_fun y := mk yl yr yL yR;
                                mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                  Sum.rec (fun i => IHxr i y) IHyr t)
                              y)
                          (xL a))
                      i y)
                  IHyl t)
              fun t =>
              Sum.rec
                (fun i =>
                  (fun a =>
                      rec (motive := fun x => PGame → PGame)
                        (fun xl xr a a IHxl IHxr y =>
                          rec
                            (fun yl yr yL yR IHyl IHyr =>
                              let_fun y := mk yl yr yL yR;
                              mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                Sum.rec (fun i => IHxr i y) IHyr t)
                            y)
                        (xR a))
                    i y)
                IHyr t)
          (yR a))
      (Sum.inl i))
[PROOFSTEP]
apply shortAdd
[GOAL]
case x.inr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
x✝¹ : Short (mk xl xr xL xR)
x✝ : Short (mk yl yr yL yR)
val✝ : yr
⊢ Short
    (Sum.rec
      (fun i =>
        (fun a =>
            rec (motive := fun x => PGame → PGame)
              (fun xl xr a a IHxl IHxr y =>
                rec
                  (fun yl yr yL yR IHyl IHyr =>
                    let_fun y := mk yl yr yL yR;
                    mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                      Sum.rec (fun i => IHxr i y) IHyr t)
                  y)
              (xR a))
          i (mk yl yr yL yR))
      (fun a =>
        rec
          (fun yl yr yL yR IHyl IHyr =>
            let_fun y := mk yl yr yL yR;
            mk (xl ⊕ yl) (xr ⊕ yr)
              (fun t =>
                Sum.rec
                  (fun i =>
                    (fun a =>
                        rec (motive := fun x => PGame → PGame)
                          (fun xl xr a a IHxl IHxr y =>
                            rec
                              (fun yl yr yL yR IHyl IHyr =>
                                let_fun y := mk yl yr yL yR;
                                mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                  Sum.rec (fun i => IHxr i y) IHyr t)
                              y)
                          (xL a))
                      i y)
                  IHyl t)
              fun t =>
              Sum.rec
                (fun i =>
                  (fun a =>
                      rec (motive := fun x => PGame → PGame)
                        (fun xl xr a a IHxl IHxr y =>
                          rec
                            (fun yl yr yL yR IHyl IHyr =>
                              let_fun y := mk yl yr yL yR;
                              mk (xl ⊕ yl) (xr ⊕ yr) (fun t => Sum.rec (fun i => IHxl i y) IHyl t) fun t =>
                                Sum.rec (fun i => IHxr i y) IHyr t)
                            y)
                        (xR a))
                    i y)
                IHyr t)
          (yR a))
      (Sum.inr val✝))
[PROOFSTEP]
change Short (mk xl xr xL xR + _)
[GOAL]
case x.inr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
x✝¹ : Short (mk xl xr xL xR)
x✝ : Short (mk yl yr yL yR)
val✝ : yr
⊢ Short (mk xl xr xL xR + yR val✝)
[PROOFSTEP]
apply shortAdd
[GOAL]
x : PGame
inst✝ : Short x
⊢ Short (bit0 x)
[PROOFSTEP]
dsimp [bit0]
[GOAL]
x : PGame
inst✝ : Short x
⊢ Short (x + x)
[PROOFSTEP]
infer_instance
[GOAL]
x : PGame
inst✝ : Short x
⊢ Short (bit1 x)
[PROOFSTEP]
dsimp [bit1]
[GOAL]
x : PGame
inst✝ : Short x
⊢ Short (bit0 x + 1)
[PROOFSTEP]
infer_instance
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
⊢ Decidable (mk xl xr xL xR ≤ mk yl yr yL yR) × Decidable (mk xl xr xL xR ⧏ mk yl yr yL yR)
[PROOFSTEP]
constructor
[GOAL]
case fst
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
⊢ Decidable (mk xl xr xL xR ≤ mk yl yr yL yR)
[PROOFSTEP]
refine' @decidable_of_iff' _ _ mk_le_mk (id _)
[GOAL]
case fst
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
⊢ Decidable ((∀ (i : xl), xL i ⧏ mk yl yr yL yR) ∧ ∀ (j : yr), mk xl xr xL xR ⧏ yR j)
[PROOFSTEP]
apply @And.decidable _ _ ?_ ?_
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
⊢ Decidable (∀ (i : xl), xL i ⧏ mk yl yr yL yR)
[PROOFSTEP]
apply @Fintype.decidableForallFintype xl _ ?_ _
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
⊢ DecidablePred fun a => xL a ⧏ mk yl yr yL yR
[PROOFSTEP]
intro i
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
i : xl
⊢ Decidable ((fun a => xL a ⧏ mk yl yr yL yR) i)
[PROOFSTEP]
apply (leLfDecidable _ _).2
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
⊢ Decidable (∀ (j : yr), mk xl xr xL xR ⧏ yR j)
[PROOFSTEP]
apply @Fintype.decidableForallFintype yr _ ?_ _
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
⊢ DecidablePred fun a => mk xl xr xL xR ⧏ yR a
[PROOFSTEP]
intro i
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
i : yr
⊢ Decidable ((fun a => mk xl xr xL xR ⧏ yR a) i)
[PROOFSTEP]
apply (leLfDecidable _ _).2
[GOAL]
case snd
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
⊢ Decidable (mk xl xr xL xR ⧏ mk yl yr yL yR)
[PROOFSTEP]
refine' @decidable_of_iff' _ _ mk_lf_mk (id _)
[GOAL]
case snd
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
⊢ Decidable ((∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR)
[PROOFSTEP]
apply @Or.decidable _ _ ?_ ?_
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
⊢ Decidable (∃ i, mk xl xr xL xR ≤ yL i)
[PROOFSTEP]
apply @Fintype.decidableExistsFintype yl _ ?_ _
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
⊢ DecidablePred fun a => mk xl xr xL xR ≤ yL a
[PROOFSTEP]
intro i
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
i : yl
⊢ Decidable ((fun a => mk xl xr xL xR ≤ yL a) i)
[PROOFSTEP]
apply (leLfDecidable _ _).1
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
⊢ Decidable (∃ j, xR j ≤ mk yl yr yL yR)
[PROOFSTEP]
apply @Fintype.decidableExistsFintype xr _ ?_ _
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
⊢ DecidablePred fun a => xR a ≤ mk yl yr yL yR
[PROOFSTEP]
intro i
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
shortx : Short (mk xl xr xL xR)
shorty : Short (mk yl yr yL yR)
i : xr
⊢ Decidable ((fun a => xR a ≤ mk yl yr yL yR) i)
[PROOFSTEP]
apply
  (leLfDecidable _ _).1
    -- Porting note: In Lean 3 `using_well_founded` didn't need this to be explicit.
[GOAL]
⊢ Short 0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Short 1
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Short 2
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Short (-2)
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Short (ofLists [0] [1])
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Short (ofLists [-2, -1] [1])
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Short (0 + 0)
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Decidable (1 ≤ 1)
[PROOFSTEP]
infer_instance
  -- No longer works since definitional reduction of well-founded definitions has been restricted.
  -- example : (0 : PGame.{u}) ≤ 0 := by decide
  -- example : (1 : PGame.{u}) ≤ 1 := by decide
