refactor(SetTheory/Ordinal): introduce natCast_pow (leanprover-community#34662)

We introduce `natCast_pow : ↑(m ^ n) = ↑m ^ n` for ordinals. We deprecate `natCast_opow : ↑(m ^ n) = ↑m ^ ↑n`, which aside from being named wrong, has an RHS which is not simp-normal.

See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ordinal.20exponentiation.20problems/with/571572044).

Author: vihdzp

Mathlib/SetTheory/Cardinal/Ordinal.lean

@@ -118,7 +118,7 @@ theorem card_opow_le_of_omega0_le_right (a : Ordinal) {b : Ordinal} (hb : ω ≤
 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
-    · rw [← natCast_opow, card_nat]
+    · 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 _ _)
   · exact (card_opow_le_of_omega0_le_left ha _).trans (le_max_right _ _)

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -1055,6 +1055,7 @@ theorem lift_ofNat (n : ℕ) [n.AtLeastTwo] :
 theorem lt_omega0 {o : Ordinal} : o < ω ↔ ∃ n : ℕ, o = n := by
   simp_rw [← Cardinal.ord_aleph0, Cardinal.lt_ord, lt_aleph0, card_eq_nat]
 
+@[simp]
 theorem nat_lt_omega0 (n : ℕ) : ↑n < ω :=
   lt_omega0.2 ⟨_, rfl⟩
 

Mathlib/SetTheory/Ordinal/Exponential.lean

@@ -500,18 +500,18 @@ theorem lt_omega0_opow_succ {a b : Ordinal} : a < ω ^ succ b ↔ ∃ n : ℕ, a
 /-! ### Interaction with `Nat.cast` -/
 
 @[simp, norm_cast]
-theorem natCast_opow (m : ℕ) : ∀ n : ℕ, ↑(m ^ n : ℕ) = (m : Ordinal) ^ (n : Ordinal)
+theorem natCast_pow (m : ℕ) : ∀ n : ℕ, ↑(m ^ n : ℕ) = (m : Ordinal) ^ n
   | 0 => by simp
-  | n + 1 => by
-    rw [pow_succ, natCast_mul, natCast_opow m n, Nat.cast_succ, add_one_eq_succ, opow_succ]
+  | n + 1 => by simp [pow_succ, natCast_pow m n]
+
+@[deprecated natCast_pow (since := "2026-01-31")]
+theorem natCast_opow (m : ℕ) : ∀ n : ℕ, ↑(m ^ n : ℕ) = (m : Ordinal) ^ (n : Ordinal) := by
+  simp
 
 theorem iSup_pow_natCast {o : Ordinal} (ho : 0 < o) : ⨆ n : ℕ, o ^ n = o ^ ω := by
-  simp_rw [← opow_natCast]
   rcases (one_le_iff_pos.2 ho).lt_or_eq with ho₁ | rfl
-  · exact apply_omega0_of_isNormal (isNormal_opow ho₁)
-  · rw [one_opow]
-    refine le_antisymm (Ordinal.iSup_le fun n => by rw [one_opow]) ?_
-    exact_mod_cast Ordinal.le_iSup _ 0
+  · simpa using apply_omega0_of_isNormal (isNormal_opow ho₁)
+  · simp
 
 @[deprecated (since := "2025-12-25")]
 alias iSup_pow := iSup_pow_natCast

Mathlib/SetTheory/Ordinal/Principal.lean

@@ -405,9 +405,7 @@ theorem mul_eq_opow_log_succ (ha : a ≠ 0) (hb : Principal (· * ·) b) (hb₂
 
 theorem principal_opow_omega0 : Principal (· ^ ·) ω := fun a b ha hb =>
   match a, b, lt_omega0.1 ha, lt_omega0.1 hb with
-  | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ => by
-    simp_rw [← natCast_opow]
-    apply nat_lt_omega0
+  | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ => by simp [← natCast_pow]
 
 theorem opow_omega0 (a1 : 1 < a) (h : a < ω) : a ^ ω = ω :=
   ((opow_le_of_isSuccLimit (one_le_iff_ne_zero.1 <| le_of_lt a1) isSuccLimit_omega0).2 fun _ hb =>

Mathlib/Tactic/NormNum/Ordinal.lean

@@ -184,7 +184,7 @@ def evalOrdinalMod : NormNumExt where
 
 lemma isNat_ordinalOPow.{u} : ∀ {a b : Ordinal.{u}} {an bn rn : ℕ},
     IsNat a an → IsNat b bn → an ^ bn = rn → IsNat (a ^ b) rn
-  | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨Eq.symm <| natCast_opow ..⟩
+  | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨(opow_natCast ..).trans (natCast_pow ..).symm⟩
 
 /-- The `norm_num` extension for homogeneous power on ordinals. -/
 @[norm_num (_ : Ordinal) ^ (_ : Ordinal)]
@@ -208,7 +208,7 @@ def evalOrdinalOPow : NormNumExt where
 
 lemma isNat_ordinalNPow.{u} : ∀ {a : Ordinal.{u}} {b an bn rn : ℕ},
     IsNat a an → IsNat b bn → an ^ bn = rn → IsNat (a ^ b) rn
-  | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨Eq.symm <| natCast_opow .. |>.trans <| opow_natCast ..⟩
+  | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨Eq.symm <| natCast_pow ..⟩
 
 /-- The `norm_num` extension for natural power on ordinals. -/
 @[norm_num (_ : Ordinal) ^ (_ : ℕ)]