From f4a9481ee46201ea7727583497f3ccc77f15f926 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= <vi.hdz.p@gmail.com>
Date: Tue, 24 Sep 2024 06:31:26 +0000
Subject: [PATCH] feat(SetTheory/*): intervals of Cardinal/Ordinal/Nimber are
 small (#16999)

---
 Mathlib/SetTheory/Cardinal/Basic.lean     |  9 ++++++---
 Mathlib/SetTheory/Ordinal/Arithmetic.lean | 15 ---------------
 Mathlib/SetTheory/Ordinal/Basic.lean      | 12 ++++++++++++
 Mathlib/SetTheory/Ordinal/Nimber.lean     | 11 ++++++-----
 4 files changed, 24 insertions(+), 23 deletions(-)

diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
index d4ea99f073058..2a607f4838215 100644
--- a/Mathlib/SetTheory/Cardinal/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -951,14 +951,17 @@ theorem bddAbove_range {ι : Type u} (f : ι → Cardinal.{max u v}) : BddAbove
     rintro a ⟨i, rfl⟩
     exact le_sum f i⟩
 
-instance (a : Cardinal.{u}) : Small.{u} (Set.Iic a) := by
+instance small_Iic (a : Cardinal.{u}) : Small.{u} (Iic a) := by
   rw [← mk_out a]
   apply @small_of_surjective (Set a.out) (Iic #a.out) _ fun x => ⟨#x, mk_set_le x⟩
   rintro ⟨x, hx⟩
   simpa using le_mk_iff_exists_set.1 hx
 
-instance (a : Cardinal.{u}) : Small.{u} (Set.Iio a) :=
-  small_subset Iio_subset_Iic_self
+instance small_Iio (a : Cardinal.{u}) : Small.{u} (Iio a) := small_subset Iio_subset_Iic_self
+instance small_Icc (a b : Cardinal.{u}) : Small.{u} (Icc a b) := small_subset Icc_subset_Iic_self
+instance small_Ico (a b : Cardinal.{u}) : Small.{u} (Ico a b) := small_subset Ico_subset_Iio_self
+instance small_Ioc (a b : Cardinal.{u}) : Small.{u} (Ioc a b) := small_subset Ioc_subset_Iic_self
+instance small_Ioo (a b : Cardinal.{u}) : Small.{u} (Ioo a b) := small_subset Ioo_subset_Iio_self
 
 /-- A set of cardinals is bounded above iff it's small, i.e. it corresponds to a usual ZFC set. -/
 theorem bddAbove_iff_small {s : Set Cardinal.{u}} : BddAbove s ↔ Small.{u} s :=
diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
index 6c48281bba80c..3fb5355737b96 100644
--- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean
+++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
@@ -1306,21 +1306,6 @@ theorem le_sup_shrink_equiv {s : Set Ordinal.{u}} (hs : Small.{u} s) (a) (ha : a
 
 -- TODO: move this together with `bddAbove_range`.
 
-instance small_Iio (o : Ordinal.{u}) : Small.{u} (Set.Iio o) :=
-  let f : o.toType → Set.Iio o :=
-    fun x => ⟨typein (α := o.toType) (· < ·) x, typein_lt_self x⟩
-  let hf : Surjective f := fun b =>
-    ⟨enum (α := o.toType) (· < ·) ⟨b.val,
-        by
-          rw [type_lt]
-          exact b.prop⟩,
-      Subtype.ext (typein_enum _ _)⟩
-  small_of_surjective hf
-
-instance small_Iic (o : Ordinal.{u}) : Small.{u} (Set.Iic o) := by
-  rw [← Iio_succ]
-  infer_instance
-
 theorem bddAbove_of_small (s : Set Ordinal.{u}) [h : Small.{u} s] : BddAbove s := by
   obtain ⟨a, ha⟩ := bddAbove_range (fun x => ((@equivShrink s h).symm x).val)
   use a
diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean
index 343348306cc66..0ebca27c90b0b 100644
--- a/Mathlib/SetTheory/Ordinal/Basic.lean
+++ b/Mathlib/SetTheory/Ordinal/Basic.lean
@@ -1008,6 +1008,18 @@ noncomputable def enumIsoToType (o : Ordinal) : Set.Iio o ≃o o.toType where
 @[deprecated (since := "2024-08-26")]
 alias enumIsoOut := enumIsoToType
 
+instance small_Iio (o : Ordinal.{u}) : Small.{u} (Iio o) :=
+  ⟨_, ⟨(enumIsoToType _).toEquiv⟩⟩
+
+instance small_Iic (o : Ordinal.{u}) : Small.{u} (Iic o) := by
+  rw [← Iio_succ]
+  exact small_Iio _
+
+instance small_Ico (a b : Ordinal.{u}) : Small.{u} (Ico a b) := small_subset Ico_subset_Iio_self
+instance small_Icc (a b : Ordinal.{u}) : Small.{u} (Icc a b) := small_subset Icc_subset_Iic_self
+instance small_Ioo (a b : Ordinal.{u}) : Small.{u} (Ioo a b) := small_subset Ioo_subset_Iio_self
+instance small_Ioc (a b : Ordinal.{u}) : Small.{u} (Ioc a b) := small_subset Ioc_subset_Iic_self
+
 /-- `o.toType` is an `OrderBot` whenever `0 < o`. -/
 def toTypeOrderBotOfPos {o : Ordinal} (ho : 0 < o) : OrderBot o.toType where
   bot_le := enum_zero_le' ho
diff --git a/Mathlib/SetTheory/Ordinal/Nimber.lean b/Mathlib/SetTheory/Ordinal/Nimber.lean
index e42c8d4e88ac3..538d61ec4400d 100644
--- a/Mathlib/SetTheory/Ordinal/Nimber.lean
+++ b/Mathlib/SetTheory/Ordinal/Nimber.lean
@@ -138,11 +138,12 @@ protected theorem not_lt_zero (a : Nimber) : ¬ a < 0 :=
 protected theorem pos_iff_ne_zero {a : Nimber} : 0 < a ↔ a ≠ 0 :=
   Ordinal.pos_iff_ne_zero
 
-instance (a : Nimber.{u}) : Small.{u} (Set.Iio a) :=
-  Ordinal.small_Iio a
-
-instance (a : Nimber.{u}) : Small.{u} (Set.Iic a) :=
-  Ordinal.small_Iic a
+instance small_Iio (a : Nimber.{u}) : Small.{u} (Set.Iio a) := Ordinal.small_Iio a
+instance small_Iic (a : Nimber.{u}) : Small.{u} (Set.Iic a) := Ordinal.small_Iic a
+instance small_Ico (a b : Nimber.{u}) : Small.{u} (Set.Ico a b) := Ordinal.small_Ico a b
+instance small_Icc (a b : Nimber.{u}) : Small.{u} (Set.Icc a b) := Ordinal.small_Icc a b
+instance small_Ioo (a b : Nimber.{u}) : Small.{u} (Set.Ioo a b) := Ordinal.small_Ioo a b
+instance small_Ioc (a b : Nimber.{u}) : Small.{u} (Set.Ioc a b) := Ordinal.small_Ioc a b
 
 end Nimber