[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

@@ -1085,11 +1085,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 := @eq_natCast_of_le_natCast o
+  grind [Nat.cast_lt]
+
 @[simp]
 theorem omega0_pos : 0 < ω :=
   natCast_lt_omega0 0