Commit 2021-04-15 04:42 c73b1653

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.