[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


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ encode (ofNat α n) = n
[PROOFSTEP]
obtain ⟨a, h, e⟩ := decode_inv (α := α) n
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
a : α
h : a ∈ decode n
e : encode a = n
⊢ encode (ofNat α n) = n
[PROOFSTEP]
rwa [ofNat_of_decode h]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type ?u.1578
β : Type ?u.1585
inst✝ : Denumerable α
e : β ≃ α
src✝ : Encodable β := Encodable.ofEquiv α e
n : ℕ
⊢ ∃ a, a ∈ decode n ∧ encode a = n
[PROOFSTEP]
simp_rw [Option.mem_def, decode_ofEquiv e, encode_ofEquiv e, decode_eq_ofNat, Option.map_some', Option.some_inj,
  exists_eq_left', Equiv.apply_symm_apply, Denumerable.encode_ofNat]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
⊢ ofNat β n = ↑e.symm (ofNat α n)
[PROOFSTEP]
letI := ofEquiv _ e
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ ofNat β n = ↑e.symm (ofNat α n)
[PROOFSTEP]
refine ofNat_of_decode ?_
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ decode n = some (↑e.symm (ofNat α n))
[PROOFSTEP]
rw [decode_ofEquiv e]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ Option.map (↑e.symm) (decode n) = some (↑e.symm (ofNat α n))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a, a ∈ decode n ∧ encode a = n
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a, a ∈ decode zero ∧ encode a = zero
case succ
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n✝ : ℕ
⊢ ∃ a, a ∈ decode (succ n✝) ∧ encode a = succ n✝
[PROOFSTEP]
case zero =>
  refine' ⟨none, _, encode_none⟩
  rw [decode_option_zero, Option.mem_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a, a ∈ decode zero ∧ encode a = zero
[PROOFSTEP]
case zero =>
  refine' ⟨none, _, encode_none⟩
  rw [decode_option_zero, Option.mem_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a, a ∈ decode zero ∧ encode a = zero
[PROOFSTEP]
refine' ⟨none, _, encode_none⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ none ∈ decode zero
[PROOFSTEP]
rw [decode_option_zero, Option.mem_def]
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n✝ : ℕ
⊢ ∃ a, a ∈ decode (succ n✝) ∧ encode a = succ n✝
[PROOFSTEP]
case succ n =>
  refine' ⟨some (ofNat α n), _, _⟩
  · rw [decode_option_succ, decode_eq_ofNat, Option.map_some', Option.mem_def]
  rw [encode_some, encode_ofNat]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a, a ∈ decode (succ n) ∧ encode a = succ n
[PROOFSTEP]
case succ n =>
  refine' ⟨some (ofNat α n), _, _⟩
  · rw [decode_option_succ, decode_eq_ofNat, Option.map_some', Option.mem_def]
  rw [encode_some, encode_ofNat]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a, a ∈ decode (succ n) ∧ encode a = succ n
[PROOFSTEP]
refine' ⟨some (ofNat α n), _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ some (ofNat α n) ∈ decode (succ n)
[PROOFSTEP]
rw [decode_option_succ, decode_eq_ofNat, Option.map_some', Option.mem_def]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ encode (some (ofNat α n)) = succ n
[PROOFSTEP]
rw [encode_some, encode_ofNat]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a, a ∈ decode n ∧ encode a = n
[PROOFSTEP]
suffices ∃ a ∈ @decodeSum α β _ _ n, encodeSum a = bit (bodd n) (div2 n) by simpa [bit_decomp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
this : ∃ a, a ∈ decodeSum n ∧ encodeSum a = bit (bodd n) (div2 n)
⊢ ∃ a, a ∈ decode n ∧ encode a = n
[PROOFSTEP]
simpa [bit_decomp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a, a ∈ decodeSum n ∧ encodeSum a = bit (bodd n) (div2 n)
[PROOFSTEP]
simp only [decodeSum, boddDiv2_eq, decode_eq_ofNat, Option.some.injEq, Option.map_some', Option.mem_def, Sum.exists]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (match (bodd n, div2 n) with
          | (false, m) => some (Sum.inl (ofNat α m))
          | (fst, m) => some (Sum.inr (ofNat β m))) =
          some (Sum.inl a) ∧
        encodeSum (Sum.inl a) = bit (bodd n) (div2 n)) ∨
    ∃ b,
      (match (bodd n, div2 n) with
          | (false, m) => some (Sum.inl (ofNat α m))
          | (fst, m) => some (Sum.inr (ofNat β m))) =
          some (Sum.inr b) ∧
        encodeSum (Sum.inr b) = bit (bodd n) (div2 n)
[PROOFSTEP]
cases bodd n
[GOAL]
case false
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (match (false, div2 n) with
          | (false, m) => some (Sum.inl (ofNat α m))
          | (fst, m) => some (Sum.inr (ofNat β m))) =
          some (Sum.inl a) ∧
        encodeSum (Sum.inl a) = bit false (div2 n)) ∨
    ∃ b,
      (match (false, div2 n) with
          | (false, m) => some (Sum.inl (ofNat α m))
          | (fst, m) => some (Sum.inr (ofNat β m))) =
          some (Sum.inr b) ∧
        encodeSum (Sum.inr b) = bit false (div2 n)
[PROOFSTEP]
simp [decodeSum, bit, encodeSum, bit0_eq_two_mul, bit1]
[GOAL]
case true
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (match (true, div2 n) with
          | (false, m) => some (Sum.inl (ofNat α m))
          | (fst, m) => some (Sum.inr (ofNat β m))) =
          some (Sum.inl a) ∧
        encodeSum (Sum.inl a) = bit true (div2 n)) ∨
    ∃ b,
      (match (true, div2 n) with
          | (false, m) => some (Sum.inl (ofNat α m))
          | (fst, m) => some (Sum.inr (ofNat β m))) =
          some (Sum.inr b) ∧
        encodeSum (Sum.inr b) = bit true (div2 n)
[PROOFSTEP]
simp [decodeSum, bit, encodeSum, bit0_eq_two_mul, bit1]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Denumerable α
inst✝¹ : Denumerable β
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ ∃ a, a ∈ decode n ∧ encode a = n
[PROOFSTEP]
simp [decodeSigma]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Denumerable α
inst✝¹ : Denumerable β
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ some (ofNat (Sigma γ) n) =
    some { fst := ofNat α (unpair n).fst, snd := ofNat (γ (ofNat α (unpair n).fst)) (unpair n).snd }
[PROOFSTEP]
rw [← decode_eq_ofNat, decode_sigma_val]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Denumerable α
inst✝¹ : Denumerable β
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ (Option.bind (decode (unpair n).fst) fun a => Option.map (Sigma.mk a) (decode (unpair n).snd)) =
    some { fst := ofNat α (unpair n).fst, snd := ofNat (γ (ofNat α (unpair n).fst)) (unpair n).snd }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ofNat (α × β) n = (ofNat α (unpair n).fst, ofNat β (unpair n).snd)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ofNat (ℕ × ℕ) = unpair
[PROOFSTEP]
funext
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
x✝ : ℕ
⊢ ofNat (ℕ × ℕ) x✝ = unpair x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
a : ℕ
ha : a ∈ s
hax : a ≥ succ ↑x
⊢ ↑x + (a - (↑x + 1)) + 1 ∈ s
[PROOFSTEP]
rwa [add_right_comm, add_tsub_cancel_of_le hax]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
this : ∀ (a : ℕ), a ∈ s → a < succ ↑x
⊢ ∀ (a : ℕ), a ∈ Multiset.filter (fun x => x ∈ s) (Multiset.range (succ ↑x)) → a ∈ s
[PROOFSTEP]
simp [-Multiset.range_succ]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
this : ∀ (a : ℕ), a ∈ s → a < succ ↑x
⊢ ∀ (x_1 : { y // y ∈ s }),
    x_1 ∈
      Multiset.toFinset
        (Multiset.pmap (fun y hy => { val := y, property := hy })
          (Multiset.filter (fun x => x ∈ s) (Multiset.range (succ ↑x)))
          (_ : ∀ (a : ℕ), a ∈ Multiset.filter (fun x => x ∈ s) (Multiset.range (succ ↑x)) → a ∈ s))
[PROOFSTEP]
simpa [Subtype.ext_iff_val, Multiset.mem_filter, -Multiset.range_succ]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x y : ↑s
h : y < x
hx : ∃ m, ↑y + m + 1 ∈ s
k : ℕ
hk : ↑x = ↑y + k + 1
this : Nat.find hx ≤ k
⊢ ↑y + Nat.find hx + 1 ≤ ↑x
[PROOFSTEP]
rw [hk]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x y : ↑s
h : y < x
hx : ∃ m, ↑y + m + 1 ∈ s
k : ℕ
hk : ↑x = ↑y + k + 1
this : Nat.find hx ≤ k
⊢ ↑y + Nat.find hx + 1 ≤ ↑y + k + 1
[PROOFSTEP]
exact add_le_add_right (add_le_add_left this _) _
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
[PROOFSTEP]
set t : List s :=
  ((List.range x).filter fun y => y ∈ s).pmap (fun (y : ℕ) (hy : y ∈ s) => ⟨y, hy⟩)
    (by intros a ha; simpa using (List.mem_filter.mp ha).2) with
  ht
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
⊢ ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s
[PROOFSTEP]
intros a ha
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
a : ℕ
ha : a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x)
⊢ a ∈ s
[PROOFSTEP]
simpa using (List.mem_filter.mp ha).2
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
[PROOFSTEP]
have hmt : ∀ {y : s}, y ∈ t ↔ y < ⟨x, hx⟩ := by simp [List.mem_filter, Subtype.ext_iff_val, ht]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
⊢ ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
[PROOFSTEP]
simp [List.mem_filter, Subtype.ext_iff_val, ht]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
[PROOFSTEP]
have wf : ∀ m : s, List.maximum t = m → ↑m < x := fun m hmax => by simpa using hmt.mp (List.maximum_mem hmax)
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
m : ↑s
hmax : List.maximum t = ↑m
⊢ ↑m < x
[PROOFSTEP]
simpa using hmt.mp (List.maximum_mem hmax)
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
[PROOFSTEP]
cases' hmax : List.maximum t with m
[GOAL]
case none
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
hmax : List.maximum t = none
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
[PROOFSTEP]
refine ⟨0, le_antisymm bot_le (le_of_not_gt fun h => List.not_mem_nil (⊥ : s) ?_)⟩
[GOAL]
case none
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
hmax : List.maximum t = none
h : { val := x✝, property := hx } > ofNat s 0
⊢ ⊥ ∈ []
[PROOFSTEP]
rwa [← List.maximum_eq_none.1 hmax, hmt]
[GOAL]
case some
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
[PROOFSTEP]
cases' ofNat_surjective_aux m.2 with a ha
[GOAL]
case some.intro
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ ∃ n, ofNat s n = { val := x✝, property := hx }
[PROOFSTEP]
refine ⟨a + 1, le_antisymm ?_ ?_⟩
[GOAL]
case some.intro.refine_1
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ ofNat s (a + 1) ≤ { val := x✝, property := hx }
[PROOFSTEP]
rw [ofNat]
[GOAL]
case some.intro.refine_2
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ { val := x✝, property := hx } ≤ ofNat s (a + 1)
[PROOFSTEP]
rw [ofNat]
[GOAL]
case some.intro.refine_1
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ succ (ofNat s a) ≤ { val := x✝, property := hx }
[PROOFSTEP]
refine succ_le_of_lt ?_
[GOAL]
case some.intro.refine_1
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ ofNat s a < { val := x✝, property := hx }
[PROOFSTEP]
rw [ha]
[GOAL]
case some.intro.refine_1
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ { val := ↑m, property := (_ : ↑m ∈ s) } < { val := x✝, property := hx }
[PROOFSTEP]
exact wf _ hmax
[GOAL]
case some.intro.refine_2
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ { val := x✝, property := hx } ≤ succ (ofNat s a)
[PROOFSTEP]
refine le_succ_of_forall_lt_le fun z hz => ?_
[GOAL]
case some.intro.refine_2
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
z : ↑s
hz : z < { val := x✝, property := hx }
⊢ z ≤ ofNat s a
[PROOFSTEP]
rw [ha]
[GOAL]
case some.intro.refine_2
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
z : ↑s
hz : z < { val := x✝, property := hx }
⊢ z ≤ { val := ↑m, property := (_ : ↑m ∈ s) }
[PROOFSTEP]
cases m
[GOAL]
case some.intro.refine_2.mk
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
a : ℕ
z : ↑s
hz : z < { val := x✝, property := hx }
val✝ : ℕ
property✝ : val✝ ∈ s
hmax : List.maximum t = some { val := val✝, property := property✝ }
ha :
  ofNat s a =
    { val := ↑{ val := val✝, property := property✝ }, property := (_ : ↑{ val := val✝, property := property✝ } ∈ s) }
⊢ z ≤ { val := ↑{ val := val✝, property := property✝ }, property := (_ : ↑{ val := val✝, property := property✝ } ∈ s) }
[PROOFSTEP]
exact List.le_maximum_of_mem (hmt.2 hz) hmax
[GOAL]
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
a✝ :
  ∀ (y : ℕ),
    (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x✝ →
      ∀ (hx : y ∈ s), ∃ n, ofNat s n = { val := y, property := hx }
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
h✝ hmax : List.maximum t = some m
t✝ : ∃ n, ofNat s n = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑m) x✝
[PROOFSTEP]
tauto
[GOAL]
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
a✝ :
  ∀ (y : ℕ),
    (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x✝ →
      ∀ (hx : y ∈ s), ∃ n, ofNat s n = { val := y, property := hx }
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
h✝ hmax : List.maximum t = some m
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑m) x✝
[PROOFSTEP]
tauto
[GOAL]
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
a✝ :
  ∀ (y : ℕ),
    (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x✝ →
      ∀ (hx : y ∈ s), ∃ n, ofNat s n = { val := y, property := hx }
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
h✝ hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑m) x✝
[PROOFSTEP]
tauto
[GOAL]
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
a✝ :
  ∀ (y : ℕ),
    (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x✝ →
      ∀ (hx : y ∈ s), ∃ n, ofNat s n = { val := y, property := hx }
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
h✝¹ hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
h✝ :
  (_ : ∃ n, ofNat s n = { val := ↑m, property := (_ : ↑m ∈ s) }) =
    (_ : ∃ n, ofNat s n = { val := ↑m, property := (_ : ↑m ∈ s) })
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑m) x✝
[PROOFSTEP]
tauto
[GOAL]
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
a✝ :
  ∀ (y : ℕ),
    (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x✝ →
      ∀ (hx : y ∈ s), ∃ n, ofNat s n = { val := y, property := hx }
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
h✝¹ hmax : List.maximum t = some m
a : ℕ
ha : ofNat s a = { val := ↑m, property := (_ : ↑m ∈ s) }
h✝ :
  (_ : ∃ n, ofNat s n = { val := ↑m, property := (_ : ↑m ∈ s) }) =
    (_ : ∃ n, ofNat s n = { val := ↑m, property := (_ : ↑m ∈ s) })
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑m) x✝
[PROOFSTEP]
tauto
[GOAL]
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x✝ : ℕ
a✝ :
  ∀ (y : ℕ),
    (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x✝ →
      ∀ (hx : y ∈ s), ∃ n, ofNat s n = { val := y, property := hx }
x : ℕ := x✝
hx : x✝ ∈ s
t : List ↑s :=
  List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
    (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
ht :
  t =
    List.pmap (fun y hy => { val := y, property := hy }) (List.filter (fun y => decide (y ∈ s)) (List.range x))
      (_ : ∀ (a : ℕ), a ∈ List.filter (fun y => decide (y ∈ s)) (List.range x) → a ∈ s)
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < { val := x, property := hx }
wf : ∀ (m : ↑s), List.maximum t = ↑m → ↑m < x
m : ↑s
h✝ hmax : List.maximum t = some m
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑m) x✝
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ Set.range (Subtype.val ∘ ofNat s) = s
[PROOFSTEP]
rw [Set.range_comp Subtype.val, ofNat_range, Set.image_univ, Subtype.range_coe]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ↑s
⊢ Nat.Subtype.toFunAux x = Finset.card (Finset.filter (fun x => x ∈ s) (Finset.range ↑x))
[PROOFSTEP]
rw [toFunAux, List.countp_eq_length_filter]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x : ↑s
⊢ List.length (List.filter (fun x => decide (x ∈ s)) (List.range ↑x)) =
    Finset.card (Finset.filter (fun x => x ∈ s) (Finset.range ↑x))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ Nat.Subtype.toFunAux (ofNat s 0) = 0
[PROOFSTEP]
rw [toFunAux_eq, card_eq_zero, eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ ∀ (x : ℕ), ¬x ∈ filter (fun x => x ∈ s) (range ↑(ofNat s 0))
[PROOFSTEP]
rintro n hn
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
hn : n ∈ filter (fun x => x ∈ s) (range ↑(ofNat s 0))
⊢ False
[PROOFSTEP]
rw [mem_filter, ofNat, mem_range] at hn
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
hn : n < ↑⊥ ∧ n ∈ s
⊢ False
[PROOFSTEP]
exact bot_le.not_lt (show (⟨n, hn.2⟩ : s) < ⊥ from hn.1)
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
⊢ Nat.Subtype.toFunAux (ofNat s (n + 1)) = n + 1
[PROOFSTEP]
have ih : toFunAux (ofNat s n) = n := right_inverse_aux n
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
⊢ Nat.Subtype.toFunAux (ofNat s (n + 1)) = n + 1
[PROOFSTEP]
have h₁ : (ofNat s n : ℕ) ∉ (range (ofNat s n)).filter (· ∈ s) := by simp
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
⊢ ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
⊢ Nat.Subtype.toFunAux (ofNat s (n + 1)) = n + 1
[PROOFSTEP]
have h₂ : (range (succ (ofNat s n))).filter (· ∈ s) = insert ↑(ofNat s n) ((range (ofNat s n)).filter (· ∈ s)) :=
  by
  simp only [Finset.ext_iff, mem_insert, mem_range, mem_filter]
  exact fun m =>
    ⟨fun h => by
      simp only [h.2, and_true_iff]
      exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1)), fun h =>
      h.elim (fun h => h.symm ▸ ⟨lt_succ_self _, (ofNat s n).prop⟩) fun h => ⟨h.1.trans (lt_succ_self _), h.2⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
⊢ filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) =
    insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))
[PROOFSTEP]
simp only [Finset.ext_iff, mem_insert, mem_range, mem_filter]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
⊢ ∀ (a : ℕ), a < ↑(succ (ofNat s n)) ∧ a ∈ s ↔ a = ↑(ofNat s n) ∨ a < ↑(ofNat s n) ∧ a ∈ s
[PROOFSTEP]
exact fun m =>
  ⟨fun h => by
    simp only [h.2, and_true_iff]
    exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1)), fun h =>
    h.elim (fun h => h.symm ▸ ⟨lt_succ_self _, (ofNat s n).prop⟩) fun h => ⟨h.1.trans (lt_succ_self _), h.2⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
m : ℕ
h : m < ↑(succ (ofNat s n)) ∧ m ∈ s
⊢ m = ↑(ofNat s n) ∨ m < ↑(ofNat s n) ∧ m ∈ s
[PROOFSTEP]
simp only [h.2, and_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
m : ℕ
h : m < ↑(succ (ofNat s n)) ∧ m ∈ s
⊢ m = ↑(ofNat s n) ∨ m < ↑(ofNat s n)
[PROOFSTEP]
exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1))
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : Nat.Subtype.toFunAux (ofNat s n) = n
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
h₂ :
  filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) =
    insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))
⊢ Nat.Subtype.toFunAux (ofNat s (n + 1)) = n + 1
[PROOFSTEP]
simp only [toFunAux_eq, ofNat, range_succ] at ih ⊢
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
h₂ :
  filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) =
    insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))
ih : card (filter (fun x => x ∈ s) (range ↑(ofNat s n))) = n
⊢ card (filter (fun x => x ∈ s) (range ↑(succ (ofNat s (Nat.add n 0))))) = n + 1
[PROOFSTEP]
conv =>
  rhs
  rw [← ih, ← card_insert_of_not_mem h₁, ← h₂]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
h₂ :
  filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) =
    insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))
ih : card (filter (fun x => x ∈ s) (range ↑(ofNat s n))) = n
| card (filter (fun x => x ∈ s) (range ↑(succ (ofNat s (Nat.add n 0))))) = n + 1
[PROOFSTEP]
  rhs
  rw [← ih, ← card_insert_of_not_mem h₁, ← h₂]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
h₂ :
  filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) =
    insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))
ih : card (filter (fun x => x ∈ s) (range ↑(ofNat s n))) = n
| card (filter (fun x => x ∈ s) (range ↑(succ (ofNat s (Nat.add n 0))))) = n + 1
[PROOFSTEP]
  rhs
  rw [← ih, ← card_insert_of_not_mem h₁, ← h₂]
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
h₂ :
  filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) =
    insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))
ih : card (filter (fun x => x ∈ s) (range ↑(ofNat s n))) = n
| card (filter (fun x => x ∈ s) (range ↑(succ (ofNat s (Nat.add n 0))))) = n + 1
[PROOFSTEP]
rhs
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
h₁ : ¬↑(ofNat s n) ∈ filter (fun x => x ∈ s) (range ↑(ofNat s n))
h₂ :
  filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) =
    insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))
ih : card (filter (fun x => x ∈ s) (range ↑(ofNat s n))) = n
| n + 1
[PROOFSTEP]
rw [← ih, ← card_insert_of_not_mem h₁, ← h₂]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
⊢ Denumerable α
[PROOFSTEP]
letI := @decidableRangeEncode α _
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
this : DecidablePred fun x => x ∈ Set.range encode := decidableRangeEncode α
⊢ Denumerable α
[PROOFSTEP]
letI : Infinite (Set.range (@encode α _)) := Infinite.of_injective _ (Equiv.ofInjective _ encode_injective).injective
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
this✝ : DecidablePred fun x => x ∈ Set.range encode := decidableRangeEncode α
this : Infinite ↑(Set.range encode) :=
  Infinite.of_injective (↑(Equiv.ofInjective encode encode_injective))
    (Equiv.injective (Equiv.ofInjective encode encode_injective))
⊢ Denumerable α
[PROOFSTEP]
letI := Nat.Subtype.denumerable (Set.range (@encode α _))
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
this✝¹ : DecidablePred fun x => x ∈ Set.range encode := decidableRangeEncode α
this✝ : Infinite ↑(Set.range encode) :=
  Infinite.of_injective (↑(Equiv.ofInjective encode encode_injective))
    (Equiv.injective (Equiv.ofInjective encode encode_injective))
this : Denumerable ↑(Set.range encode) := Subtype.denumerable (Set.range encode)
⊢ Denumerable α
[PROOFSTEP]
exact Denumerable.ofEquiv (Set.range (@encode α _)) (equivRangeEncode α)
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Countable α
inst✝² : Infinite α
inst✝¹ : Countable β
inst✝ : Infinite β
⊢ Nonempty (α ≃ β)
[PROOFSTEP]
cases nonempty_denumerable α
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝³ : Countable α
inst✝² : Infinite α
inst✝¹ : Countable β
inst✝ : Infinite β
val✝ : Denumerable α
⊢ Nonempty (α ≃ β)
[PROOFSTEP]
cases nonempty_denumerable β
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Countable α
inst✝² : Infinite α
inst✝¹ : Countable β
inst✝ : Infinite β
val✝¹ : Denumerable α
val✝ : Denumerable β
⊢ Nonempty (α ≃ β)
[PROOFSTEP]
exact ⟨(Denumerable.eqv _).trans (Denumerable.eqv _).symm⟩