-- Mathlib/SetTheory/Game/Short.lean
theorem short_birthday (x : PGame.{u}) : [Short x] → x.birthday < Ordinal.omega0

Proof state:
case mk.mk
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
⊢ (Ordinal.lsub fun i => (xL i).birthday) < Ordinal.omega0 ∧ (Ordinal.lsub fun i => (xR i).birthday) < Ordinal.omega0

Tactic:
constructor

Result:
case mk.mk.left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
⊢ (Ordinal.lsub fun i => (xL i).birthday) < Ordinal.omega0

case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
⊢ (Ordinal.lsub fun i => (xR i).birthday) < Ordinal.omega0

Proof state:
case mk.mk
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
⊢ (mk xl xr xL xR).birthday < Ordinal.omega0

Tactic:
rw [birthday, max_lt_iff]

Result:
case mk.mk
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
⊢ (Ordinal.lsub fun i => (xL i).birthday) < Ordinal.omega0 ∧ (Ordinal.lsub fun i => (xR i).birthday) < Ordinal.omega0

Proof state:
case mk.mk.left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
⊢ (Ordinal.lsub fun i => (xL i).birthday) < Ordinal.omega0

case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
⊢ (Ordinal.lsub fun i => (xR i).birthday) < Ordinal.omega0

Tactic:
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]

Result:
case mk.mk.left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
i : xl
⊢ (xL i).birthday < Ordinal.omega0

case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
i : xr
⊢ (xR i).birthday < Ordinal.omega0

Proof state:
case mk
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
hs : (mk xl xr xL xR).Short
⊢ (mk xl xr xL xR).birthday < Ordinal.omega0

Tactic:
rcases hs with ⟨sL, sR⟩

Result:
case mk.mk
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
⊢ (mk xl xr xL xR).birthday < Ordinal.omega0

Proof state:
case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
i : xr
⊢ (xR i).birthday < Ordinal.omega0

Tactic:
apply ihr

Result:
no goals

Proof state:
case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
⊢ (Ordinal.lsub fun i => (xR i).birthday) < Cardinal.aleph0.ord

Tactic:
refine
  Cardinal.lsub_lt_ord_of_isRegular.{u, u} Cardinal.isRegular_aleph0
    (Cardinal.lt_aleph0_of_finite _) fun i => ?_

Result:
case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
i : xr
⊢ (xR i).birthday < Cardinal.aleph0.ord

Proof state:
case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
⊢ (Ordinal.lsub fun i => (xR i).birthday) < Ordinal.omega0

Tactic:
rw [← Cardinal.ord_aleph0]

Result:
case mk.mk.right
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
⊢ (Ordinal.lsub fun i => (xR i).birthday) < Cardinal.aleph0.ord

Proof state:
case mk
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
⊢ ∀ [inst : (mk xl xr xL xR).Short], (mk xl xr xL xR).birthday < Ordinal.omega0

Tactic:
intro hs

Result:
case mk
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
hs : (mk xl xr xL xR).Short
⊢ (mk xl xr xL xR).birthday < Ordinal.omega0

Proof state:
case mk.mk.left
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
ihl : ∀ (a : xl) [inst : (xL a).Short], (xL a).birthday < Ordinal.omega0
ihr : ∀ (a : xr) [inst : (xR a).Short], (xR a).birthday < Ordinal.omega0
inst✝¹ : Fintype xl
inst✝ : Fintype xr
sL : (i : xl) → (xL i).Short
sR : (j : xr) → (xR j).Short
i : xl
⊢ (xL i).birthday < Ordinal.omega0

Tactic:
apply ihl

Result:
no goals