chore(set_theory/cardinal/ordinal): follow your linter (#16265)
Editing `set_theory.cardinal.ordinal`, I noticed that the linter was unhappy. So, I thought of pleasing it. I followed its instructions, but, admittedly, I do not know if this is a good change or not!
I replaced some `fintype` assumptions by `finite` ones and changed one proof as a consequence.
