[GOAL]
x : PGame
⊢ birthday x = max (lsub fun i => birthday (moveLeft x i)) (lsub fun i => birthday (moveRight x i))
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ birthday (mk α✝ β✝ a✝¹ a✝) =
    max (lsub fun i => birthday (moveLeft (mk α✝ β✝ a✝¹ a✝) i)) (lsub fun i => birthday (moveRight (mk α✝ β✝ a✝¹ a✝) i))
[PROOFSTEP]
rw [birthday]
[GOAL]
case mk
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ max (lsub fun i => birthday (a✝¹ i)) (lsub fun i => birthday (a✝ i)) =
    max (lsub fun i => birthday (moveLeft (mk α✝ β✝ a✝¹ a✝) i)) (lsub fun i => birthday (moveRight (mk α✝ β✝ a✝¹ a✝) i))
[PROOFSTEP]
rfl
[GOAL]
x : PGame
i : LeftMoves x
⊢ birthday (moveLeft x i) < birthday x
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : LeftMoves (mk α✝ β✝ a✝¹ a✝)
⊢ birthday (moveLeft (mk α✝ β✝ a✝¹ a✝) i) < birthday (mk α✝ β✝ a✝¹ a✝)
[PROOFSTEP]
rw [birthday]
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : LeftMoves (mk α✝ β✝ a✝¹ a✝)
⊢ birthday (moveLeft (mk α✝ β✝ a✝¹ a✝) i) < max (lsub fun i => birthday (a✝¹ i)) (lsub fun i => birthday (a✝ i))
[PROOFSTEP]
exact lt_max_of_lt_left (lt_lsub _ i)
[GOAL]
x : PGame
i : RightMoves x
⊢ birthday (moveRight x i) < birthday x
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : RightMoves (mk α✝ β✝ a✝¹ a✝)
⊢ birthday (moveRight (mk α✝ β✝ a✝¹ a✝) i) < birthday (mk α✝ β✝ a✝¹ a✝)
[PROOFSTEP]
rw [birthday]
[GOAL]
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : RightMoves (mk α✝ β✝ a✝¹ a✝)
⊢ birthday (moveRight (mk α✝ β✝ a✝¹ a✝) i) < max (lsub fun i => birthday (a✝¹ i)) (lsub fun i => birthday (a✝ i))
[PROOFSTEP]
exact lt_max_of_lt_right (lt_lsub _ i)
[GOAL]
x : PGame
o : Ordinal.{u_1}
⊢ o < birthday x ↔ (∃ i, o ≤ birthday (moveLeft x i)) ∨ ∃ i, o ≤ birthday (moveRight x i)
[PROOFSTEP]
constructor
[GOAL]
case mp
x : PGame
o : Ordinal.{u_1}
⊢ o < birthday x → (∃ i, o ≤ birthday (moveLeft x i)) ∨ ∃ i, o ≤ birthday (moveRight x i)
[PROOFSTEP]
rw [birthday_def]
[GOAL]
case mp
x : PGame
o : Ordinal.{u_1}
⊢ o < max (lsub fun i => birthday (moveLeft x i)) (lsub fun i => birthday (moveRight x i)) →
    (∃ i, o ≤ birthday (moveLeft x i)) ∨ ∃ i, o ≤ birthday (moveRight x i)
[PROOFSTEP]
intro h
[GOAL]
case mp
x : PGame
o : Ordinal.{u_1}
h : o < max (lsub fun i => birthday (moveLeft x i)) (lsub fun i => birthday (moveRight x i))
⊢ (∃ i, o ≤ birthday (moveLeft x i)) ∨ ∃ i, o ≤ birthday (moveRight x i)
[PROOFSTEP]
cases' lt_max_iff.1 h with h' h'
[GOAL]
case mp.inl
x : PGame
o : Ordinal.{u_1}
h : o < max (lsub fun i => birthday (moveLeft x i)) (lsub fun i => birthday (moveRight x i))
h' : o < lsub fun i => birthday (moveLeft x i)
⊢ (∃ i, o ≤ birthday (moveLeft x i)) ∨ ∃ i, o ≤ birthday (moveRight x i)
[PROOFSTEP]
left
[GOAL]
case mp.inl.h
x : PGame
o : Ordinal.{u_1}
h : o < max (lsub fun i => birthday (moveLeft x i)) (lsub fun i => birthday (moveRight x i))
h' : o < lsub fun i => birthday (moveLeft x i)
⊢ ∃ i, o ≤ birthday (moveLeft x i)
[PROOFSTEP]
rwa [lt_lsub_iff] at h' 
[GOAL]
case mp.inr
x : PGame
o : Ordinal.{u_1}
h : o < max (lsub fun i => birthday (moveLeft x i)) (lsub fun i => birthday (moveRight x i))
h' : o < lsub fun i => birthday (moveRight x i)
⊢ (∃ i, o ≤ birthday (moveLeft x i)) ∨ ∃ i, o ≤ birthday (moveRight x i)
[PROOFSTEP]
right
[GOAL]
case mp.inr.h
x : PGame
o : Ordinal.{u_1}
h : o < max (lsub fun i => birthday (moveLeft x i)) (lsub fun i => birthday (moveRight x i))
h' : o < lsub fun i => birthday (moveRight x i)
⊢ ∃ i, o ≤ birthday (moveRight x i)
[PROOFSTEP]
rwa [lt_lsub_iff] at h' 
[GOAL]
case mpr
x : PGame
o : Ordinal.{u_1}
⊢ ((∃ i, o ≤ birthday (moveLeft x i)) ∨ ∃ i, o ≤ birthday (moveRight x i)) → o < birthday x
[PROOFSTEP]
rintro (⟨i, hi⟩ | ⟨i, hi⟩)
[GOAL]
case mpr.inl.intro
x : PGame
o : Ordinal.{u_1}
i : LeftMoves x
hi : o ≤ birthday (moveLeft x i)
⊢ o < birthday x
[PROOFSTEP]
exact hi.trans_lt (birthday_moveLeft_lt i)
[GOAL]
case mpr.inr.intro
x : PGame
o : Ordinal.{u_1}
i : RightMoves x
hi : o ≤ birthday (moveRight x i)
⊢ o < birthday x
[PROOFSTEP]
exact hi.trans_lt (birthday_moveRight_lt i)
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ birthday (PGame.mk xl xr xL xR) = birthday (PGame.mk yl yr yL yR)
[PROOFSTEP]
unfold birthday
[GOAL]
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ max (lsub fun i => birthday (xL i)) (lsub fun i => birthday (xR i)) =
    max (lsub fun i => birthday (yL i)) (lsub fun i => birthday (yR i))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (lsub fun i => birthday (xL i)) = lsub fun i => birthday (yL i)
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (lsub fun i => birthday (xR i)) = lsub fun i => birthday (yR i)
[PROOFSTEP]
all_goals
  apply lsub_eq_of_range_eq.{u, u, u}
  ext i; constructor
[GOAL]
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (lsub fun i => birthday (xL i)) = lsub fun i => birthday (yL i)
[PROOFSTEP]
apply lsub_eq_of_range_eq.{u, u, u}
[GOAL]
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (Set.range fun i => birthday (xL i)) = Set.range fun i => birthday (yL i)
[PROOFSTEP]
ext i
[GOAL]
case e_a.h
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (xL i)) ↔ i ∈ Set.range fun i => birthday (yL i)
[PROOFSTEP]
constructor
[GOAL]
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (lsub fun i => birthday (xR i)) = lsub fun i => birthday (yR i)
[PROOFSTEP]
apply lsub_eq_of_range_eq.{u, u, u}
[GOAL]
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (Set.range fun i => birthday (xR i)) = Set.range fun i => birthday (yR i)
[PROOFSTEP]
ext i
[GOAL]
case e_a.h
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (xR i)) ↔ i ∈ Set.range fun i => birthday (yR i)
[PROOFSTEP]
constructor
[GOAL]
case e_a.h.mp
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (xL i)) → i ∈ Set.range fun i => birthday (yL i)
case e_a.h.mpr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (yL i)) → i ∈ Set.range fun i => birthday (xL i)
case e_a.h.mp
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (xR i)) → i ∈ Set.range fun i => birthday (yR i)
case e_a.h.mpr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (yR i)) → i ∈ Set.range fun i => birthday (xR i)
[PROOFSTEP]
all_goals rintro ⟨j, rfl⟩
[GOAL]
case e_a.h.mp
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (xL i)) → i ∈ Set.range fun i => birthday (yL i)
[PROOFSTEP]
rintro ⟨j, rfl⟩
[GOAL]
case e_a.h.mpr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (yL i)) → i ∈ Set.range fun i => birthday (xL i)
[PROOFSTEP]
rintro ⟨j, rfl⟩
[GOAL]
case e_a.h.mp
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (xR i)) → i ∈ Set.range fun i => birthday (yR i)
[PROOFSTEP]
rintro ⟨j, rfl⟩
[GOAL]
case e_a.h.mpr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => birthday (yR i)) → i ∈ Set.range fun i => birthday (xR i)
[PROOFSTEP]
rintro ⟨j, rfl⟩
[GOAL]
case e_a.h.mp.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : xl
⊢ (fun i => birthday (xL i)) j ∈ Set.range fun i => birthday (yL i)
[PROOFSTEP]
exact ⟨_, (r.moveLeft j).birthday_congr.symm⟩
[GOAL]
case e_a.h.mpr.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : yl
⊢ (fun i => birthday (yL i)) j ∈ Set.range fun i => birthday (xL i)
[PROOFSTEP]
exact ⟨_, (r.moveLeftSymm j).birthday_congr⟩
[GOAL]
case e_a.h.mp.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : xr
⊢ (fun i => birthday (xR i)) j ∈ Set.range fun i => birthday (yR i)
[PROOFSTEP]
exact ⟨_, (r.moveRight j).birthday_congr.symm⟩
[GOAL]
case e_a.h.mpr.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : yr
⊢ (fun i => birthday (yR i)) j ∈ Set.range fun i => birthday (xR i)
[PROOFSTEP]
exact ⟨_, (r.moveRightSymm j).birthday_congr⟩
[GOAL]
x : PGame
⊢ birthday x = 0 ↔ IsEmpty (LeftMoves x) ∧ IsEmpty (RightMoves x)
[PROOFSTEP]
rw [birthday_def, max_eq_zero, lsub_eq_zero_iff, lsub_eq_zero_iff]
[GOAL]
⊢ birthday 0 = 0
[PROOFSTEP]
simp [inferInstanceAs (IsEmpty PEmpty)]
[GOAL]
⊢ birthday 1 = 1
[PROOFSTEP]
rw [birthday_def]
[GOAL]
⊢ max (lsub fun i => birthday (moveLeft 1 i)) (lsub fun i => birthday (moveRight 1 i)) = 1
[PROOFSTEP]
simp
[GOAL]
⊢ birthday star = 1
[PROOFSTEP]
rw [birthday_def]
[GOAL]
⊢ max (lsub fun i => birthday (moveLeft star i)) (lsub fun i => birthday (moveRight star i)) = 1
[PROOFSTEP]
simp
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ birthday (-mk xl xr xL xR) = birthday (mk xl xr xL xR)
[PROOFSTEP]
rw [birthday_def, birthday_def, max_comm]
[GOAL]
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ max (lsub fun i => birthday (moveRight (-mk xl xr xL xR) i)) (lsub fun i => birthday (moveLeft (-mk xl xr xL xR) i)) =
    max (lsub fun i => birthday (moveLeft (mk xl xr xL xR) i)) (lsub fun i => birthday (moveRight (mk xl xr xL xR) i))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_f
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ (fun i => birthday (moveRight (-mk xl xr xL xR) i)) = fun i => birthday (moveLeft (mk xl xr xL xR) i)
[PROOFSTEP]
funext
[GOAL]
case e_a.e_f
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ (fun i => birthday (moveLeft (-mk xl xr xL xR) i)) = fun i => birthday (moveRight (mk xl xr xL xR) i)
[PROOFSTEP]
funext
[GOAL]
case e_a.e_f.h
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
x✝ : RightMoves (-mk xl xr xL xR)
⊢ birthday (moveRight (-mk xl xr xL xR) x✝) = birthday (moveLeft (mk xl xr xL xR) x✝)
[PROOFSTEP]
apply neg_birthday
[GOAL]
case e_a.e_f.h
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
x✝ : LeftMoves (-mk xl xr xL xR)
⊢ birthday (moveLeft (-mk xl xr xL xR) x✝) = birthday (moveRight (mk xl xr xL xR) x✝)
[PROOFSTEP]
apply neg_birthday
[GOAL]
o : Ordinal.{u_1}
⊢ birthday (toPGame o) = o
[PROOFSTEP]
induction' o using Ordinal.induction with o IH
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
⊢ birthday (toPGame o) = o
[PROOFSTEP]
rw [toPGame_def, PGame.birthday]
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
⊢ max (lsub fun i => birthday (toPGame (typein (fun x x_1 => x < x_1) i))) (lsub fun i => birthday (PEmpty.elim i)) = o
[PROOFSTEP]
simp only [lsub_empty, max_zero_right]
  -- Porting note: was `nth_rw 1 [← lsub_typein o]`
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
⊢ (lsub fun i => birthday (toPGame (typein (fun x x_1 => x < x_1) i))) = o
[PROOFSTEP]
conv_rhs => rw [← lsub_typein o]
[GOAL]
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
| o
[PROOFSTEP]
rw [← lsub_typein o]
[GOAL]
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
| o
[PROOFSTEP]
rw [← lsub_typein o]
[GOAL]
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
| o
[PROOFSTEP]
rw [← lsub_typein o]
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
⊢ (lsub fun i => birthday (toPGame (typein (fun x x_1 => x < x_1) i))) = lsub (typein fun x x_1 => x < x_1)
[PROOFSTEP]
congr with x
[GOAL]
case h.e_f.h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (toPGame k) = k
x : (Quotient.out o).α
⊢ birthday (toPGame (typein (fun x x_1 => x < x_1) x)) = typein (fun x x_1 => x < x_1) x
[PROOFSTEP]
exact IH _ (typein_lt_self x)
[GOAL]
xl β✝ : Type u_1
xL : xl → PGame
a✝ : β✝ → PGame
i : LeftMoves (mk xl β✝ xL a✝)
⊢ moveLeft (mk xl β✝ xL a✝) i ≤
    moveLeft (toPGame (birthday (mk xl β✝ xL a✝)))
      (↑toLeftMovesToPGame
        { val := birthday (moveLeft (mk xl β✝ xL a✝) i),
          property := (_ : birthday (moveLeft (mk xl β✝ xL a✝) i) < birthday (mk xl β✝ xL a✝)) })
[PROOFSTEP]
simp [le_birthday (xL i)]
[GOAL]
a b x : PGame
⊢ -toPGame (birthday x) ≤ x
[PROOFSTEP]
simpa only [neg_birthday, ← neg_le_iff] using le_birthday (-x)
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ birthday (mk xl xr xL xR + mk yl yr yL yR) = birthday (mk xl xr xL xR) ♯ birthday (mk yl yr yL yR)
[PROOFSTEP]
rw [birthday_def, nadd_def]
  -- Porting note: `simp` doesn't apply
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (lsub fun i => birthday (moveLeft (mk xl xr xL xR + mk yl yr yL yR) i))
      (lsub fun i => birthday (moveRight (mk xl xr xL xR + mk yl yr yL yR) i)) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
erw [lsub_sum, lsub_sum]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max
      (max (lsub fun a => birthday (moveLeft (mk xl xr xL xR + mk yl yr yL yR) (Sum.inl a)))
        (lsub fun b => birthday (moveLeft (mk xl xr xL xR + mk yl yr yL yR) (Sum.inr b))))
      (max (lsub fun a => birthday (moveRight (mk xl xr xL xR + mk yl yr yL yR) (Sum.inl a)))
        (lsub fun b => birthday (moveRight (mk xl xr xL xR + mk yl yr yL yR) (Sum.inr b)))) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
simp only [lsub_sum, mk_add_moveLeft_inl, moveLeft_mk, mk_add_moveLeft_inr, mk_add_moveRight_inl, moveRight_mk,
  mk_add_moveRight_inr]
  -- Porting note: Originally `simp only [birthday_add]`, but this causes an error in
      -- `termination_by`. Use a workaround.
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (max (lsub fun a => birthday (xL a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
      (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b))) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
conv_lhs => left; left; right; intro a; rw [birthday_add (xL a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (max (lsub fun a => birthday (xL a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
left; left; right; intro a; rw [birthday_add (xL a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (max (lsub fun a => birthday (xL a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
left; left; right; intro a; rw [birthday_add (xL a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (max (lsub fun a => birthday (xL a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
left
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (lsub fun a => birthday (xL a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b))
[PROOFSTEP]
left
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| lsub fun a => birthday (xL a + mk yl yr yL yR)
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| fun a => birthday (xL a + mk yl yr yL yR)
[PROOFSTEP]
intro a
[GOAL]
case h
a✝ b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
a : xl
| birthday (xL a + mk yl yr yL yR)
[PROOFSTEP]
rw [birthday_add (xL a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
      (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b))) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
conv_lhs => left; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yL b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
left; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yL b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
left; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yL b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
left
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yL b))
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| lsub fun b => birthday (mk xl xr xL xR + yL b)
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| fun b => birthday (mk xl xr xL xR + yL b)
[PROOFSTEP]
intro b
[GOAL]
case h
a b✝ x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
b : yl
| birthday (mk xl xr xL xR + yL b)
[PROOFSTEP]
rw [birthday_add ⟨xl, xr, xL, xR⟩ (yL b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max
      (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
        (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
      (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b))) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
conv_lhs => right; left; right; intro a; rw [birthday_add (xR a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max
    (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
right; left; right; intro a; rw [birthday_add (xR a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max
    (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
right; left; right; intro a; rw [birthday_add (xR a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max
    (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
    (max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (lsub fun a => birthday (xR a + mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b))
[PROOFSTEP]
left
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| lsub fun a => birthday (xR a + mk yl yr yL yR)
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| fun a => birthday (xR a + mk yl yr yL yR)
[PROOFSTEP]
intro a
[GOAL]
case h
a✝ b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
a : xr
| birthday (xR a + mk yl yr yL yR)
[PROOFSTEP]
rw [birthday_add (xR a) ⟨yl, yr, yL, yR⟩]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max
      (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
        (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
      (max (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
        (lsub fun b => birthday (mk xl xr xL xR + yR b))) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
conv_lhs => right; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yR b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max
    (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
    (max (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
right; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yR b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max
    (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
    (max (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
right; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yR b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max
    (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
    (max (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b)))
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| max (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)) (lsub fun b => birthday (mk xl xr xL xR + yR b))
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| lsub fun b => birthday (mk xl xr xL xR + yR b)
[PROOFSTEP]
right
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
| fun b => birthday (mk xl xr xL xR + yR b)
[PROOFSTEP]
intro b
[GOAL]
case h
a b✝ x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
b : yr
| birthday (mk xl xr xL xR + yR b)
[PROOFSTEP]
rw [birthday_add ⟨xl, xr, xL, xR⟩ (yR b)]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max
      (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
        (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b)))
      (max (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
        (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
rw [max_max_max_comm]
[GOAL]
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max
      (max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
        (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)))
      (max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
        (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))) =
    max (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR))
      (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b')
[PROOFSTEP]
congr
[GOAL]
case e_a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)) =
    blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case e_a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b)) =
    blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b'
[PROOFSTEP]
apply le_antisymm
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)) ≤
    blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR)
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR)) ≤
    max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b)) ≤
    blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b'
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b') ≤
    max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))
[PROOFSTEP]
any_goals
  exact
    max_le_iff.2
      ⟨lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveLeft_lt _),
        lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveRight_lt _)⟩
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR)) ≤
    blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR)
[PROOFSTEP]
exact
  max_le_iff.2
    ⟨lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveLeft_lt _),
      lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveRight_lt _)⟩
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR)) ≤
    max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
[PROOFSTEP]
exact
  max_le_iff.2
    ⟨lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveLeft_lt _),
      lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveRight_lt _)⟩
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b)) ≤
    blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b'
[PROOFSTEP]
exact
  max_le_iff.2
    ⟨lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveLeft_lt _),
      lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveRight_lt _)⟩
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b') ≤
    max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))
[PROOFSTEP]
exact
  max_le_iff.2
    ⟨lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveLeft_lt _),
      lsub_le_iff.2 fun i => lt_blsub _ _ (birthday_moveRight_lt _)⟩
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR)) ≤
    max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b') ≤
    max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))
[PROOFSTEP]
all_goals
  refine blsub_le_iff.2 fun i hi => ?_
  rcases lt_birthday_iff.1 hi with (⟨j, hj⟩ | ⟨j, hj⟩)
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk xl xr xL xR)) fun a' x => a' ♯ birthday (mk yl yr yL yR)) ≤
    max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
[PROOFSTEP]
refine blsub_le_iff.2 fun i hi => ?_
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i < birthday (mk xl xr xL xR)
⊢ i ♯ birthday (mk yl yr yL yR) <
    max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
[PROOFSTEP]
rcases lt_birthday_iff.1 hi with (⟨j, hj⟩ | ⟨j, hj⟩)
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ (blsub (birthday (mk yl yr yL yR)) fun b' x => birthday (mk xl xr xL xR) ♯ b') ≤
    max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))
[PROOFSTEP]
refine blsub_le_iff.2 fun i hi => ?_
[GOAL]
case e_a.a
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i < birthday (mk yl yr yL yR)
⊢ birthday (mk xl xr xL xR) ♯ i <
    max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))
[PROOFSTEP]
rcases lt_birthday_iff.1 hi with (⟨j, hj⟩ | ⟨j, hj⟩)
[GOAL]
case e_a.a.inl.intro
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i < birthday (mk xl xr xL xR)
j : LeftMoves (mk xl xr xL xR)
hj : i ≤ birthday (moveLeft (mk xl xr xL xR) j)
⊢ i ♯ birthday (mk yl yr yL yR) <
    max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
[PROOFSTEP]
exact lt_max_of_lt_left ((nadd_le_nadd_right hj _).trans_lt (lt_lsub _ _))
[GOAL]
case e_a.a.inr.intro
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i < birthday (mk xl xr xL xR)
j : RightMoves (mk xl xr xL xR)
hj : i ≤ birthday (moveRight (mk xl xr xL xR) j)
⊢ i ♯ birthday (mk yl yr yL yR) <
    max (lsub fun a => birthday (xL a) ♯ birthday (mk yl yr yL yR))
      (lsub fun a => birthday (xR a) ♯ birthday (mk yl yr yL yR))
[PROOFSTEP]
exact lt_max_of_lt_right ((nadd_le_nadd_right hj _).trans_lt (lt_lsub _ _))
[GOAL]
case e_a.a.inl.intro
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i < birthday (mk yl yr yL yR)
j : LeftMoves (mk yl yr yL yR)
hj : i ≤ birthday (moveLeft (mk yl yr yL yR) j)
⊢ birthday (mk xl xr xL xR) ♯ i <
    max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))
[PROOFSTEP]
exact lt_max_of_lt_left ((nadd_le_nadd_left hj _).trans_lt (lt_lsub _ _))
[GOAL]
case e_a.a.inr.intro
a b x : PGame
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i < birthday (mk yl yr yL yR)
j : RightMoves (mk yl yr yL yR)
hj : i ≤ birthday (moveRight (mk yl yr yL yR) j)
⊢ birthday (mk xl xr xL xR) ♯ i <
    max (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yL b))
      (lsub fun b => birthday (mk xl xr xL xR) ♯ birthday (yR b))
[PROOFSTEP]
exact lt_max_of_lt_right ((nadd_le_nadd_left hj _).trans_lt (lt_lsub _ _))
[GOAL]
a b x : PGame
⊢ birthday (a + 0) = birthday a
[PROOFSTEP]
simp
[GOAL]
a b x : PGame
⊢ birthday (0 + a) = birthday a
[PROOFSTEP]
simp
[GOAL]
a b x : PGame
⊢ birthday (a + 1) = Order.succ (birthday a)
[PROOFSTEP]
simp
[GOAL]
a b x : PGame
⊢ birthday (1 + a) = Order.succ (birthday a)
[PROOFSTEP]
simp
[GOAL]
a b x : PGame
n : ℕ
⊢ birthday ↑(n + 1) = ↑(n + 1)
[PROOFSTEP]
simp [birthday_nat_cast]
[GOAL]
a b x : PGame
n : ℕ
⊢ birthday (a + ↑n) = birthday a + ↑n
[PROOFSTEP]
simp
[GOAL]
a b x : PGame
n : ℕ
⊢ birthday (↑n + a) = birthday a + ↑n
[PROOFSTEP]
simp
