Ordinal exponentiation problems

Stream: mathlib4

[Violeta Hernández]

Working with nimbers I came across a really annoying simp failure:

import Mathlib.SetTheory.Ordinal.Exponential

example : (2 : Ordinal) ^ (2 ^ n : ℕ) = 2 ^ (2 : Ordinal) ^ (n : ℕ) := by
  -- simp -- fails
  -- norm_cast -- fails too
  simp [← Ordinal.opow_natCast]

There's clearly a missing lemma or tag, but I don't really know which one it'd be. Any ideas?

[Dexin Zhang]

It seems to be Nat.cast_pow?

[Dexin Zhang]

This works

@[norm_cast]
lemma cast_pow (m : ℕ) : ∀ n : ℕ, ↑(m ^ n) = (m ^ n : Ordinal) := by
  simp [Ordinal.opow_natCast]

example : (2 : Ordinal) ^ (2 ^ n : ℕ) = 2 ^ (2 : Ordinal) ^ (n : ℕ) := by
  norm_cast

[Yury G. Kudryashov]

If you want a simp lemma to work with numeral literals, you need to add ofNat(n) versions.

[Violeta Hernández]

Oh, I think I see the issue. docs#Ordinal.natCast_opow, besides being named wrong, doesn't have a simp-normal RHS.

[Violeta Hernández]

Yury G. Kudryashov said:

If you want a simp lemma to work with numeral literals, you need to add ofNat(n) versions.

There are two natural numbers here, does that mean I need two ofNat versions, one for each?

[Violeta Hernández]

This should get fixed by #34662