-- Mathlib/SetTheory/Game/Birthday.lean
theorem small_setOf_birthday_lt (o : Ordinal) : Small.{u} {x : Game.{u} // birthday x < o}

Proof state:
case h.inr.inr
o : Ordinal.{u}
IH : ∀ k < o, Small.{u, u + 1} { x // x.birthday < k }
S : Set Game := ⋃ a ∈ Set.Iio o, {x | x.birthday < a}
H : Small.{u, u + 1} ↑S := small_biUnion (Set.Iio o) fun a h => {x | x.birthday < a}
ho : o.IsLimit
⊢ Small.{u, u + 1} { x // x.birthday < o }

Tactic:
convert H

Result:
case h.e'_1.h.e'_2.h.a
o : Ordinal.{u}
IH : ∀ k < o, Small.{u, u + 1} { x // x.birthday < k }
S : Set Game := ⋃ a ∈ Set.Iio o, {x | x.birthday < a}
H : Small.{u, u + 1} ↑S := small_biUnion (Set.Iio o) fun a h => {x | x.birthday < a}
ho : o.IsLimit
x✝ : Game
⊢ x✝.birthday < o ↔ S x✝

Proof state:
y : PGame
IH : ∀ k < Order.succ (birthday ⟦y⟧), Small.{u, u + 1} { x // x.birthday < k }
S : Set Game := ⋃ a ∈ Set.Iio (Order.succ (birthday ⟦y⟧)), {x | x.birthday < a}
H : Small.{u, u + 1} ↑S := small_biUnion (Set.Iio (Order.succ (birthday ⟦y⟧))) fun a h => {x | x.birthday < a}
f : Set ↑S × Set ↑S → Game :=
  fun g =>
    ⟦PGame.mk (Shrink.{u, u + 1} ↑g.1) (Shrink.{u, u + 1} ↑g.2) (fun x => Quotient.out ↑↑((equivShrink ↑g.1).symm x))
        fun x => Quotient.out ↑↑((equivShrink ↑g.2).symm x)⟧
hy' : y.birthday = birthday ⟦y⟧
i : y.LeftMoves
⊢ ⟦y.moveLeft i⟧ ∈ S

Tactic:
suffices ∃ b ≤ y.birthday, birthday ⟦y.moveLeft i⟧ < b by simpa [S, hy'] using this

Result:
y : PGame
IH : ∀ k < Order.succ (birthday ⟦y⟧), Small.{u, u + 1} { x // x.birthday < k }
S : Set Game := ⋃ a ∈ Set.Iio (Order.succ (birthday ⟦y⟧)), {x | x.birthday < a}
H : Small.{u, u + 1} ↑S := small_biUnion (Set.Iio (Order.succ (birthday ⟦y⟧))) fun a h => {x | x.birthday < a}
f : Set ↑S × Set ↑S → Game :=
  fun g =>
    ⟦PGame.mk (Shrink.{u, u + 1} ↑g.1) (Shrink.{u, u + 1} ↑g.2) (fun x => Quotient.out ↑↑((equivShrink ↑g.1).symm x))
        fun x => Quotient.out ↑↑((equivShrink ↑g.2).symm x)⟧
hy' : y.birthday = birthday ⟦y⟧
i : y.LeftMoves
⊢ ∃ b ≤ y.birthday, birthday ⟦y.moveLeft i⟧ < b

Proof state:
case h.inr.inl.intro.convert_2
x : Game
IH : ∀ k < Order.succ x.birthday, Small.{u, u + 1} { x // x.birthday < k }
S : Set Game := ⋃ a ∈ Set.Iio (Order.succ x.birthday), {x | x.birthday < a}
H : Small.{u, u + 1} ↑S := small_biUnion (Set.Iio (Order.succ x.birthday)) fun a h => {x | x.birthday < a}
f : Set ↑S × Set ↑S → Game :=
  fun g =>
    ⟦PGame.mk (Shrink.{u, u + 1} ↑g.1) (Shrink.{u, u + 1} ↑g.2) (fun x => Quotient.out ↑↑((equivShrink ↑g.1).symm x))
        fun x => Quotient.out ↑↑((equivShrink ↑g.2).symm x)⟧
⊢ x ∈ Set.range f

Tactic:
obtain ⟨y, rfl, hy'⟩ := birthday_eq_pGameBirthday x

Result:
case h.inr.inl.intro.convert_2.intro.intro
y : PGame
IH : ∀ k < Order.succ (birthday ⟦y⟧), Small.{u, u + 1} { x // x.birthday < k }
S : Set Game := ⋃ a ∈ Set.Iio (Order.succ (birthday ⟦y⟧)), {x | x.birthday < a}
H : Small.{u, u + 1} ↑S := small_biUnion (Set.Iio (Order.succ (birthday ⟦y⟧))) fun a h => {x | x.birthday < a}
f : Set ↑S × Set ↑S → Game :=
  fun g =>
    ⟦PGame.mk (Shrink.{u, u + 1} ↑g.1) (Shrink.{u, u + 1} ↑g.2) (fun x => Quotient.out ↑↑((equivShrink ↑g.1).symm x))
        fun x => Quotient.out ↑↑((equivShrink ↑g.2).symm x)⟧
hy' : y.birthday = birthday ⟦y⟧
⊢ ⟦y⟧ ∈ Set.range f

Proof state:
case h.inr.inl.intro.convert_2.intro.intro
y : PGame
IH : ∀ k < Order.succ (birthday ⟦y⟧), Small.{u, u + 1} { x // x.birthday < k }
S : Set Game := ⋃ a ∈ Set.Iio (Order.succ (birthday ⟦y⟧)), {x | x.birthday < a}
H : Small.{u, u + 1} ↑S := small_biUnion (Set.Iio (Order.succ (birthday ⟦y⟧))) fun a h => {x | x.birthday < a}
f : Set ↑S × Set ↑S → Game :=
  fun g =>
    ⟦PGame.mk (Shrink.{u, u + 1} ↑g.1) (Shrink.{u, u + 1} ↑g.2) (fun x => Quotient.out ↑↑((equivShrink ↑g.1).symm x))
        fun x => Quotient.out ↑↑((equivShrink ↑g.2).symm x)⟧
hy' : y.birthday = birthday ⟦y⟧
⊢ ⟦y⟧ ∈ Set.range f

Tactic:
refine ⟨⟨{z | ∃ i, ⟦y.moveLeft i⟧ = z.1}, {z | ∃ i, ⟦y.moveRight i⟧ = z.1}⟩, ?_⟩

Result:
case h.inr.inl.intro.convert_2.intro.intro
y : PGame
IH : ∀ k < Order.succ (birthday ⟦y⟧), Small.{u, u + 1} { x // x.birthday < k }
S : Set Game := ⋃ a ∈ Set.Iio (Order.succ (birthday ⟦y⟧)), {x | x.birthday < a}
H : Small.{u, u + 1} ↑S := small_biUnion (Set.Iio (Order.succ (birthday ⟦y⟧))) fun a h => {x | x.birthday < a}
f : Set ↑S × Set ↑S → Game :=
  fun g =>
    ⟦PGame.mk (Shrink.{u, u + 1} ↑g.1) (Shrink.{u, u + 1} ↑g.2) (fun x => Quotient.out ↑↑((equivShrink ↑g.1).symm x))
        fun x => Quotient.out ↑↑((equivShrink ↑g.2).symm x)⟧
hy' : y.birthday = birthday ⟦y⟧
⊢ f ({z | ∃ i, ⟦y.moveLeft i⟧ = ↑z}, {z | ∃ i, ⟦y.moveRight i⟧ = ↑z}) = ⟦y⟧

Proof state:
case h.inr.inl.intro
a : Ordinal.{u}
IH : ∀ k < Order.succ a, Small.{u, u + 1} { x // x.birthday < k }
S : Set Game := ⋃ a_1 ∈ Set.Iio (Order.succ a), {x | x.birthday < a_1}
H : Small.{u, u + 1} ↑S := small_biUnion (Set.Iio (Order.succ a)) fun a_1 h => {x | x.birthday < a_1}
⊢ Small.{u, u + 1} { x // x.birthday < a ∨ x.birthday = a }

Tactic:
convert small_union.{u} {x | birthday x < a} {x | birthday x = a}

Result:
case h.inr.inl.intro.convert_1
a : Ordinal.{u}
IH : ∀ k < Order.succ a, Small.{u, u + 1} { x // x.birthday < k }
S : Set Game := ⋃ a_1 ∈ Set.Iio (Order.succ a), {x | x.birthday < a_1}
H : Small.{u, u + 1} ↑S := small_biUnion (Set.Iio (Order.succ a)) fun a_1 h => {x | x.birthday < a_1}
⊢ Small.{u, u + 1} ↑{x | x.birthday < a}

case h.inr.inl.intro.convert_2
a : Ordinal.{u}
IH : ∀ k < Order.succ a, Small.{u, u + 1} { x // x.birthday < k }
S : Set Game := ⋃ a_1 ∈ Set.Iio (Order.succ a), {x | x.birthday < a_1}
H : Small.{u, u + 1} ↑S := small_biUnion (Set.Iio (Order.succ a)) fun a_1 h => {x | x.birthday < a_1}
⊢ Small.{u, u + 1} ↑{x | x.birthday = a}

Proof state:
case h.e'_1.h.e'_2.h.a
o : Ordinal.{u}
IH : ∀ k < o, Small.{u, u + 1} { x // x.birthday < k }
S : Set Game := ⋃ a ∈ Set.Iio o, {x | x.birthday < a}
H : Small.{u, u + 1} ↑S := small_biUnion (Set.Iio o) fun a h => {x | x.birthday < a}
ho : o.IsLimit
x✝ : Game
⊢ x✝.birthday < o ↔ S x✝

Tactic:
change birthday _ < o ↔ ∃ a, _

Result:
case h.e'_1.h.e'_2.h.a
o : Ordinal.{u}
IH : ∀ k < o, Small.{u, u + 1} { x // x.birthday < k }
S : Set Game := ⋃ a ∈ Set.Iio o, {x | x.birthday < a}
H : Small.{u, u + 1} ↑S := small_biUnion (Set.Iio o) fun a h => {x | x.birthday < a}
ho : o.IsLimit
x✝ : Game
⊢ x✝.birthday < o ↔ ∃ a ∈ Set.range fun a => ⋃ (_ : a ∈ Set.Iio o), {x | x.birthday < a}, x✝ ∈ a