mathlib

d53bbb6e - feat(data/fin_enum): `fin_enum` class for finite types with an enumeration order (#1368)

feat(data/fin_enum): `fin_enum` class for finite types with an enumeration order (#1368) * feat(data/enum): `enumerable` class for finite types with an enumeration order * little fixes * Update enum.lean * Update enum.lean * Update finset.lean * add documentation * Update src/data/enum.lean Co-Authored-By: Scott Morrison <scott@tqft.net> * Update src/data/enum.lean [skip ci] Co-Authored-By: Scott Morrison <scott@tqft.net> * Update fin.lean [skip ci[ * Update enum.lean * Update enum.lean * Update fin.lean [skip ci] * Update enum.lean * Update src/data/enum.lean [skip ci] Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update interactive.lean [skip ci] * Rename enum.lean to fin_enum.lean [skip ci] * add `mono using` to doc/tactics.md [skip ci] * update to Lean 3.5.1 * address lint comments * Update src/data/fin_enum.lean Co-Authored-By: Scott Morrison <scott@tqft.net> * Update fin_enum.lean * Apply suggestions from code review Co-Authored-By: Scott Morrison <scott@tqft.net> * remove unneeded lemmas * add `nodup_to_list` Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>