[Merged by Bors] - feat: lemmas on ordinal Nat.cast

Mathlib/SetTheory/Cardinal/Ordinal.lean

@@ -110,15 +110,15 @@ theorem card_opow_le_of_omega0_le_left {a : Ordinal} (ha : ω ≤ a) (b : Ordina
 
 theorem card_opow_le_of_omega0_le_right (a : Ordinal) {b : Ordinal} (hb : ω ≤ b) :
     (a ^ b).card ≤ max a.card b.card := by
-  obtain ⟨n, rfl⟩ | ha := eq_nat_or_omega0_le a
+  obtain ⟨n, rfl⟩ | ha := eq_natCast_or_omega0_le a
   · apply (card_le_card <| opow_le_opow_left b (natCast_lt_omega0 n).le).trans
     apply (card_opow_le_of_omega0_le_left le_rfl _).trans
     simp [hb]
   · exact card_opow_le_of_omega0_le_left ha b
 
 theorem card_opow_le (a b : Ordinal) : (a ^ b).card ≤ max ℵ₀ (max a.card b.card) := by
-  obtain ⟨n, rfl⟩ | ha := eq_nat_or_omega0_le a
-  · obtain ⟨m, rfl⟩ | hb := eq_nat_or_omega0_le b
+  obtain ⟨n, rfl⟩ | ha := eq_natCast_or_omega0_le a
+  · obtain ⟨m, rfl⟩ | hb := eq_natCast_or_omega0_le b
     · rw [opow_natCast, ← natCast_pow, card_nat]
       exact le_max_of_le_left natCast_le_aleph0
     · exact (card_opow_le_of_omega0_le_right _ hb).trans (le_max_right _ _)

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -1102,11 +1102,22 @@ theorem natCast_lt_omega0 (n : ℕ) : ↑n < ω :=
 theorem enum_lt_nat (x : ℕ) : enum LT.lt ⟨x, by simp⟩ = x := by
   simp [← typein_inj LT.lt]
 
-theorem eq_nat_or_omega0_le (o : Ordinal) : (∃ n : ℕ, o = n) ∨ ω ≤ o := by
+theorem eq_natCast_of_le_natCast {a : Ordinal} {b : ℕ} (h : a ≤ b) : ∃ c : ℕ, a = c :=
+  lt_omega0.1 (h.trans_lt (natCast_lt_omega0 b))
+
+theorem eq_natCast_or_omega0_le (o : Ordinal) : (∃ n : ℕ, o = n) ∨ ω ≤ o := by
   obtain ho | ho := lt_or_ge o ω
   · exact Or.inl <| lt_omega0.1 ho
   · exact Or.inr ho
 
+@[deprecated (since := "2026-03-12")] alias eq_nat_or_omega0_le := eq_natCast_or_omega0_le
+
+@[simp]
+theorem natCast_image_Iio (n : ℕ) : Nat.cast '' Set.Iio n = Set.Iio (n : Ordinal) := by
+  ext o
+  have (h : o ≤ n) := eq_natCast_of_le_natCast h
+  grind [Nat.cast_lt]
+
 @[simp]
 theorem omega0_pos : 0 < ω :=
   natCast_lt_omega0 0

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -337,18 +337,14 @@ instance : OrderBot Ordinal where
   bot := 0
   bot_le o := inductionOn o fun _ r _ ↦ (InitialSeg.ofIsEmpty _ r).ordinal_type_le
 
-@[simp]
-theorem bot_eq_zero : (⊥ : Ordinal) = 0 :=
-  rfl
-
-instance instIsEmptyIioZero : IsEmpty (Iio (0 : Ordinal)) := by
-  simp [← bot_eq_zero]
+@[simp] theorem bot_eq_zero : (⊥ : Ordinal) = 0 := rfl
+theorem Iio_zero : Set.Iio (0 : Ordinal) = ∅ := by simp
+instance : IsEmpty (Iio (0 : Ordinal)) := by simp
 
 @[deprecated nonpos_iff_eq_zero (since := "2025-11-21")]
 protected theorem le_zero {o : Ordinal} : o ≤ 0 ↔ o = 0 :=
   le_bot_iff
 
-
 @[deprecated not_neg (since := "2025-11-21")]
 protected theorem not_lt_zero (o : Ordinal) : ¬o < 0 :=
   not_lt_bot
@@ -925,6 +921,17 @@ theorem lt_one_iff_zero {a : Ordinal} : a < 1 ↔ a = 0 := by
 theorem le_one_iff {a : Ordinal} : a ≤ 1 ↔ a = 0 ∨ a = 1 := by
   simpa using @le_succ_bot_iff _ _ _ a _
 
+@[simp]
+theorem Iio_one : Set.Iio (1 : Ordinal) = {0} := by
+  rw [← zero_add 1, ← Order.succ_eq_add_one, Order.Iio_succ]
+  exact Set.Iic_bot
+
+@[simp]
+theorem Iio_two : Set.Iio (2 : Ordinal) = {0, 1} := by
+  rw [← succ_one, Order.Iio_succ]
+  ext
+  simp [le_one_iff]
+
 -- TODO: deprecate
 theorem card_succ (o : Ordinal) : card (succ o) = card o + 1 := by
   simp