feat: values of preAleph.symm (leanprover-community#39713)

For a cardinal `c`, `preAleph.symm c` returns the ordinal index of `c`, within the well-order of cardinals.

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Co-authored-by: Aaron Liu <aaronliu2008@outlook.com>
Co-authored-by: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com>
Co-authored-by: Thomas Browning <13339017+tb65536@users.noreply.github.com>
Co-authored-by: Yi.Yuan <kysyy1@126.com>
Co-authored-by: mathlib-splicebot[bot] <261196803+mathlib-splicebot[bot]@users.noreply.github.com>
Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
Co-authored-by: Wenrong Zou <141128015+WenrongZou@users.noreply.github.com>
Co-authored-by: Manuel Candales <42380156+manuelcandales@users.noreply.github.com>
Co-authored-by: Sebastien Gouezel <10818434+sgouezel@users.noreply.github.com>
Co-authored-by: Justus Springer <50165510+justus-springer@users.noreply.github.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Co-authored-by: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com>
Co-authored-by: Lua Viana Reis <me@lua.blog.br>
Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>
Co-authored-by: mathlib-update-dependencies[bot] <258990618+mathlib-update-dependencies[bot]@users.noreply.github.com>
Co-authored-by: Michael Rothgang <10105016+grunweg@users.noreply.github.com>
Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>
Co-authored-by: Garmelon <11077553+Garmelon@users.noreply.github.com>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
Co-authored-by: Jon Eugster <9141564+joneugster@users.noreply.github.com>
Co-authored-by: damiano <adomani@gmail.com>
Co-authored-by: Bhavik Mehta <29959226+b-mehta@users.noreply.github.com>
Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Co-authored-by: Xavier Généreux <20421163+xgenereux@users.noreply.github.com>
Co-authored-by: Weiyi Wang <wwylele@gmail.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

Author: 28 people

Mathlib/SetTheory/Cardinal/Aleph.lean

@@ -342,13 +342,31 @@ theorem preAleph_succ (o : Ordinal) : preAleph (succ o) = succ (preAleph o) :=
   preAleph.map_succ o
 
 @[simp]
-theorem preAleph_nat (n : ℕ) : preAleph n = n := by
+theorem preAleph_natCast (n : ℕ) : preAleph n = n := by
   rw [← card_preOmega, preOmega_natCast, card_nat]
 
+@[simp]
+theorem preAleph_ofNat (n : ℕ) [n.AtLeastTwo] : preAleph ofNat(n) = ofNat(n) :=
+  preAleph_natCast n
+
+@[simp]
+theorem preAleph_symm_natCast (n : ℕ) : preAleph.symm n = n := by
+  simp [OrderIso.symm_apply_eq]
+
+@[simp]
+theorem preAleph_symm_ofNat (n : ℕ) [n.AtLeastTwo] : preAleph.symm ofNat(n) = ofNat(n) :=
+  preAleph_symm_natCast n
+
+@[deprecated (since := "2026-05-22")] alias preAleph_nat := preAleph_natCast
+
 @[simp]
 theorem preAleph_omega0 : preAleph ω = ℵ₀ := by
   rw [← card_preOmega, preOmega_omega0, card_omega0]
 
+@[simp]
+theorem preAleph_symm_aleph0 : preAleph.symm ℵ₀ = ω := by
+  simp [OrderIso.symm_apply_eq]
+
 @[simp]
 theorem preAleph_pos {o : Ordinal} : 0 < preAleph o ↔ 0 < o := by
   rw [← preAleph_zero, preAleph_lt_preAleph]
@@ -397,7 +415,7 @@ theorem preAleph_le_of_strictMono {f : Ordinal → Cardinal} (hf : StrictMono f)
 
 For a version including finite cardinals, see `Cardinal.preAleph`. -/
 def aleph : Ordinal ↪o Cardinal :=
-  (OrderEmbedding.addLeft ω).trans preAleph.toOrderEmbedding
+  (OrderEmbedding.addLeft ω).trans preAleph
 
 @[inherit_doc] scoped notation "ℵ_ " => aleph
 recommended_spelling "aleph" for "ℵ_" in [aleph, «termℵ_»]
@@ -413,6 +431,10 @@ theorem aleph_eq_preAleph (o : Ordinal) : ℵ_ o = preAleph (ω + o) :=
 theorem _root_.Ordinal.card_omega (o : Ordinal) : (ω_ o).card = ℵ_ o :=
   rfl
 
+@[simp]
+theorem preAleph_symm_aleph (o : Ordinal) : preAleph.symm (ℵ_ o) = ω + o :=
+  preAleph.symm_apply_apply _
+
 @[simp]
 theorem ord_aleph (o : Ordinal) : (ℵ_ o).ord = ω_ o :=
   ord_preAleph _

Mathlib/SetTheory/Cardinal/Regular.lean

@@ -431,6 +431,9 @@ theorem IsInaccessible.preAleph_ord (hc : IsInaccessible c) : preAleph c.ord = c
   ((preAleph_le_preBeth _).trans hc.preBeth_ord.le).antisymm
     (preAleph.strictMono.comp ord_strictMono).le_apply
 
+theorem IsInaccessible.preAleph_symm_eq_ord (hc : IsInaccessible c) : preAleph.symm c = c.ord := by
+  rw [OrderIso.symm_apply_eq, hc.preAleph_ord]
+
 theorem IsInaccessible.aleph_ord (hc : IsInaccessible c) : ℵ_ c.ord = c :=
   ((aleph_le_beth _).trans hc.beth_ord.le).antisymm (aleph.strictMono.comp ord_strictMono).le_apply
 
@@ -452,6 +455,10 @@ theorem beth_univ : ℶ_ Ordinal.univ.{u, v} = univ.{u, v} := by
 theorem preAleph_univ : preAleph Ordinal.univ.{u, v} = univ.{u, v} := by
   simpa using IsInaccessible.univ.preAleph_ord
 
+@[simp]
+theorem preAleph_symm_univ : preAleph.symm univ.{u, v} = Ordinal.univ.{u, v} := by
+  simp [OrderIso.symm_apply_eq]
+
 @[simp]
 theorem aleph_univ : ℵ_ Ordinal.univ.{u, v} = univ.{u, v} := by
   simpa using IsInaccessible.univ.aleph_ord