Commit 2020-08-31 13:17 9e9e318c

feat(data/fin): simplify fin.mk (#3996) After the recent changes to make fin n a subtype, expressions involving fin.mk were not getting simplified as they used to be, since the simp lemmas are for the anonymous constructor, which is subtype.mk not fin.mk. Add a simp lemma converting fin.mk to the anonymous constructor. In particular, unsimplified expressions involving fin.mk were coming out of fin_cases (I think this comes from fin_range in data/list/range.lean using fin.mk). I don't know if that should be avoiding creating the fin.mk expressions in the first place, but simplifying them seems a good idea in any case.