Commit 2021-05-16 18:58 b98d8408

feat(category_theory/category): initialize simps (#7605) Initialize @[simps] so that it works better for category. It just makes the names of the generated lemmas shorter. Add @[simps] to product categories.