-- 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.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⟧

Tactic:
apply PGame.game_eq <| PGame.Equiv.of_exists _ _ _ _ <;> intro i

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 :
  (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)).LeftMoves
⊢ ∃ j,
    (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)).moveLeft
        i ≈
      y.moveLeft j

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 :
  (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)).RightMoves
⊢ ∃ j,
    (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
        i ≈
      y.moveRight j

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
⊢ ∃ i_1,
    (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)).moveLeft
        i_1 ≈
      y.moveLeft i

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
⊢ ∃ i_1,
    (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
        i_1 ≈
      y.moveRight i

Proof state:
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}
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 | x.birthday = a} ⊆ Set.range f

Tactic:
rintro x rfl

Result:
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