Mathlib.Data.Fintype.Small
source
That is, any α with [Fintype α] is equivalent to a type in any universe.
α
[Fintype α]