feat: Small sets of games/surreals are bounded (#10458)

Finish forwarding porting leanprover-community/mathlib#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>

Mathlib/SetTheory/Game/Basic.lean

@@ -7,7 +7,7 @@ import Mathlib.Data.Int.Basic
 import Mathlib.SetTheory.Game.PGame
 import Mathlib.Tactic.Abel
 
-#align_import set_theory.game.basic from "leanprover-community/mathlib"@"6623e6af705e97002a9054c1c05a980180276fc1"
+#align_import set_theory.game.basic from "leanprover-community/mathlib"@"8900d545017cd21961daa2a1734bb658ef52c618"
 
 /-!
 # Combinatorial games.
@@ -202,6 +202,30 @@ instance orderedAddCommGroup : OrderedAddCommGroup Game :=
     add_le_add_left := @add_le_add_left _ _ _ Game.covariantClass_add_le }
 #align game.ordered_add_comm_group SetTheory.Game.orderedAddCommGroup
 
+/-- A small family of games is bounded above. -/
+lemma bddAbove_range_of_small {ι : Type*} [Small.{u} ι] (f : ι → Game.{u}) :
+    BddAbove (Set.range f) := by
+  obtain ⟨x, hx⟩ := PGame.bddAbove_range_of_small (Quotient.out ∘ f)
+  refine ⟨⟦x⟧, Set.forall_mem_range.2 fun i ↦ ?_⟩
+  simpa [PGame.le_iff_game_le] using hx $ Set.mem_range_self i
+
+/-- A small set of games is bounded above. -/
+lemma bddAbove_of_small (s : Set Game.{u}) [Small.{u} s] : BddAbove s := by
+  simpa using bddAbove_range_of_small (Subtype.val : s → Game.{u})
+#align game.bdd_above_of_small SetTheory.Game.bddAbove_of_small
+
+/-- A small family of games is bounded below. -/
+lemma bddBelow_range_of_small {ι : Type*} [Small.{u} ι] (f : ι → Game.{u}) :
+    BddBelow (Set.range f) := by
+  obtain ⟨x, hx⟩ := PGame.bddBelow_range_of_small (Quotient.out ∘ f)
+  refine ⟨⟦x⟧, Set.forall_mem_range.2 fun i ↦ ?_⟩
+  simpa [PGame.le_iff_game_le] using hx $ Set.mem_range_self i
+
+/-- A small set of games is bounded below. -/
+lemma bddBelow_of_small (s : Set Game.{u}) [Small.{u} s] : BddBelow s := by
+  simpa using bddBelow_range_of_small (Subtype.val : s → Game.{u})
+#align game.bdd_below_of_small SetTheory.Game.bddBelow_of_small
+
 end Game
 
 namespace PGame

Mathlib/SetTheory/Surreal/Basic.lean

@@ -6,7 +6,7 @@ Authors: Mario Carneiro, Scott Morrison
 import Mathlib.Algebra.Order.Hom.Monoid
 import Mathlib.SetTheory.Game.Ordinal
 
-#align_import set_theory.surreal.basic from "leanprover-community/mathlib"@"ee02a30e209a2a77b93eac1254e8c66e76192f54"
+#align_import set_theory.surreal.basic from "leanprover-community/mathlib"@"8900d545017cd21961daa2a1734bb658ef52c618"
 
 /-!
 # Surreal numbers
@@ -322,6 +322,9 @@ instance instLE : LE Surreal :=
   ⟨lift₂ (fun x y _ _ => x ≤ y) fun _ _ _ _ hx hy => propext (le_congr hx hy)⟩
 #align surreal.has_le Surreal.instLE
 
+@[simp]
+lemma mk_le_mk {x y : PGame.{u}} {hx hy} : mk x hx ≤ mk y hy ↔ x ≤ y := Iff.rfl
+
 instance instLT : LT Surreal :=
   ⟨lift₂ (fun x y _ _ => x < y) fun _ _ _ _ hx hy => propext (lt_congr hx hy)⟩
 #align surreal.has_lt Surreal.instLT
@@ -388,6 +391,53 @@ theorem nat_toGame : ∀ n : ℕ, toGame n = n :=
   map_natCast' _ one_toGame
 #align surreal.nat_to_game Surreal.nat_toGame
 
+#noalign upper_bound_numeric
+#noalign lower_bound_numeric
+
+/-- A small family of surreals is bounded above. -/
+lemma bddAbove_range_of_small {ι : Type*} [Small.{u} ι] (f : ι → Surreal.{u}) :
+    BddAbove (Set.range f) := by
+  induction' f using Quotient.induction_on_pi with f
+  let g : ι → PGame.{u} := Subtype.val ∘ f
+  have hg (i) : (g i).Numeric := Subtype.prop _
+  conv in (⟦f _⟧) =>
+    change mk (g i) (hg i)
+  clear_value g
+  clear f
+  let x : PGame.{u} := ⟨Σ i, (g <| (equivShrink.{u} ι).symm i).LeftMoves, PEmpty,
+    fun x ↦ moveLeft _ x.2, PEmpty.elim⟩
+  refine ⟨mk x (.mk (by simp [x]) (fun _ ↦ (hg _).moveLeft _) (by simp [x])),
+    Set.forall_mem_range.2 fun i ↦ ?_⟩
+  rw [mk_le_mk, ← (equivShrink ι).symm_apply_apply i, le_iff_forall_lf]
+  simpa [x] using fun j ↦ @moveLeft_lf x ⟨equivShrink ι i, j⟩
+
+/-- A small set of surreals is bounded above. -/
+lemma bddAbove_of_small (s : Set Surreal.{u}) [Small.{u} s] : BddAbove s := by
+  simpa using bddAbove_range_of_small (Subtype.val : s → Surreal.{u})
+#align surreal.bdd_above_of_small Surreal.bddAbove_of_small
+
+/-- A small family of surreals is bounded below. -/
+lemma bddBelow_range_of_small {ι : Type*} [Small.{u} ι] (f : ι → Surreal.{u}) :
+    BddBelow (Set.range f) := by
+  induction' f using Quotient.induction_on_pi with f
+  let g : ι → PGame.{u} := Subtype.val ∘ f
+  have hg (i) : (g i).Numeric := Subtype.prop _
+  conv in (⟦f _⟧) =>
+    change mk (g i) (hg i)
+  clear_value g
+  clear f
+  let x : PGame.{u} := ⟨PEmpty, Σ i, (g <| (equivShrink.{u} ι).symm i).RightMoves,
+    PEmpty.elim, fun x ↦ moveRight _ x.2⟩
+  refine ⟨mk x (.mk (by simp [x]) (by simp [x]) (fun _ ↦ (hg _).moveRight _) ),
+    Set.forall_mem_range.2 fun i ↦ ?_⟩
+  rw [mk_le_mk, ← (equivShrink ι).symm_apply_apply i, le_iff_forall_lf]
+  simpa [x] using fun j ↦ @lf_moveRight x ⟨equivShrink ι i, j⟩
+
+/-- A small set of surreals is bounded below. -/
+lemma bddBelow_of_small (s : Set Surreal.{u}) [Small.{u} s] : BddBelow s := by
+  simpa using bddBelow_range_of_small (Subtype.val : s → Surreal.{u})
+#align surreal.bdd_below_of_small Surreal.bddBelow_of_small
+
 end Surreal
 
 open Surreal