chore(data/fin,data/finset): a few lemmas (#7168)
* `fin.heq_fun_iff`: use `Sort*` instead of `Type*`;
* `fin.cast_refl`: take `h : n = n := rfl` as an argument;
* `fin.cast_to_equiv`, `fin.cast_eq_cast`: relate `fin.cast` to `_root_.cast`;
* `finset.map_cast_heq`: new lemma;
* `finset.subset_univ`: add `@[simp]`;
* `card_finset_fin_le`, `fintype.card_finset_len`, `fin.prod_const` : new lemmas;
* `order_iso.refl`: new definition.
