Lean 4: How can I specify that out of two universe variables, one is larger than the other?

Before Mathlib 4 was finished, I decided to implement my own ordinals, but this was as I was learning Lean 4, so my Ordinal type had type Type 1 instead of the proper Type u + 1. Now I'm trying to rewrite my code to use as much of Mathlib as possible, and make it as general as possible. I have a function

def ordinalMap.notInjection
(f: Ordinal → T)
:
¬ isInjection f
:=
...


and to make it general, the variable T should be able to live in different universes. The problem is that if I just add two universe variables like this:

def ordinalMap.notInjection.{u,t}
{T: Type t}
(f: Ordinal.{u} → T)
:
¬ isInjection f
:=
...


the theorem becomes false -- even the identity function on ordinals is a counter-example. The statement is only true if T has a smaller universe level than (or equal to?) that of the ordinals. (For the proof I adapted the reasoning I found on Wikipedia's article on the Hartogs number. Intuitively, there is always "more ordinals" of Ordinal: Type u + 1 then of objects of T: Type u).

I tried adding this constraint as an argument to the function:

def ordinalMap.notInjection.{u,t}
{tu: t < u}
...


but I get the error "typeclass instance problem is stuck, it is often due to metavariables".

Then I tried to make the type of f Ordinal.{max u (t + 1)} → T, which I suppose would work, but it makes u not necessarily the universe level of the ordinals. Is this the right approach? Or is there something better?

(Lastly, if this function is implemented already somewhere in Mathlib, or can be easily proven using it, I'll be glad to know. I'm afraid I'm not (yet?) very effective at searching in the library.)

• A MWE might be helpful here complete with the definition (or imports) of Ordinal. But also I guess it is not clear how you hope to use a universe polymorphic version of the ordinalMap.notInjection theorem. (Side note: calling it a definition is confusing.) Without an application in mind, I’m not sure if you can know the right approach. But maybe the right approach is just your original ordinalMap.notInjection theorem. If one has specific universes v < u, they can just ulift T: Type v to Type u and then use your theorem, no? Commented Dec 10, 2023 at 13:06
• Commented Dec 10, 2023 at 13:09
• Oh, sorry I thought your original was universe polymorphic but with only one universe variable u, used for both Type and Ordinal. I guess that is what I was suggesting, but the last option also makes sense. I think those are your two options. Commented Dec 10, 2023 at 13:12

theorem not_injective_of_ordinal {α : Type u}  (f : Ordinal.{u} → α) :

theorem not_injective_of_ordinal_of_small {α : Type v}  [Small.{u, v} α] (f : Ordinal.{u} → α) :

Notice how they use the type class Small to handle comparing universe levels.