chore(set_theory/ordinal): Minor golf in `card` (#12298)
chore(set_theory/ordinal): Minor golf in `card` (#12298)

This was suggested by @b-mehta.





leanprover-community/mathlib,leanprover-community/mathlib