feat(data/fintype): prove `card (subtype p) ≤ card α` (#1383)
* feat(data/fintype): prove `card (subtype p) ≤ card α`
* Add `cardinal.mk_le_of_subtype`
* Rename `mk_le_of_subtype` to `mk_subtype_le`, use it in `mk_set_le`
Earlier both `mk_subtype_le` and `mk_set_le` took `set α` as an
argument. Now `mk_subtype_le` takes `α → Prop`.
