chore(set_theory/cardinal): more simp, fix LHS/RHS (#10212)
While `coe (fintype.card α)` is a larger expression than `#α`, it allows us to compute the cardinality of a finite type provided that we have a `simp` lemma for `fintype.card α`. It also plays well with lemmas about coercions from `nat` and `cardinal.lift`.
* rename `cardinal.fintype_card` to `cardinal.mk_fintype`, make it a `@[simp]` lemma;
* deduce other cases (`bool`, `Prop`, `unique`, `is_empty`) from it;
* rename `cardinal.finset_card` to `cardinal.mk_finset`, swap LHS/RHS;
* rename `ordinal.fintype_card` to `ordinal.type_fintype`.
