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

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.RightMoves
⊢ ∃ b ≤ y.birthday, birthday ⟦y.moveRight i⟧ < b

Tactic:
refine ⟨_, le_rfl, ?_⟩

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.RightMoves
⊢ birthday ⟦y.moveRight i⟧ < y.birthday

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
⊢ ∃ b ≤ y.birthday, birthday ⟦y.moveLeft i⟧ < b

Tactic:
refine ⟨_, le_rfl, ?_⟩

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
⊢ birthday ⟦y.moveLeft i⟧ < y.birthday

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.RightMoves
⊢ (PGame.mk (Shrink.{u, u + 1} ↑({z | ∃ i, ⟦y.moveLeft i⟧ = ↑z}, {z | ∃ i, ⟦y.moveRight i⟧ = ↑z}).1)
          (Shrink.{u, u + 1} ↑({z | ∃ i, ⟦y.moveLeft i⟧ = ↑z}, {z | ∃ i, ⟦y.moveRight i⟧ = ↑z}).2)
          (fun x =>
            Quotient.out ↑↑((equivShrink ↑({z | ∃ i, ⟦y.moveLeft i⟧ = ↑z}, {z | ∃ i, ⟦y.moveRight i⟧ = ↑z}).1).symm x))
          fun x =>
          Quotient.out
            ↑↑((equivShrink ↑({z | ∃ i, ⟦y.moveLeft i⟧ = ↑z}, {z | ∃ i, ⟦y.moveRight i⟧ = ↑z}).2).symm x)).moveRight
      ((equivShrink ↑({z | ∃ i, ⟦y.moveLeft i⟧ = ↑z}, {z | ∃ i, ⟦y.moveRight i⟧ = ↑z}).2)
        ⟨⟨⟦y.moveRight i⟧, ?m.124830⟩, ⋯⟩) ≈
    y.moveRight i

Tactic:
simpa using Quotient.mk_out _

Result:
no goals

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
this : ∃ b ≤ y.birthday, birthday ⟦y.moveLeft i⟧ < b
⊢ ⟦y.moveLeft i⟧ ∈ S

Tactic:
simpa [S, hy'] using this

Result:
no goals