[Merged by Bors] - chore(CategoryTheory/EssentiallySmall): lower priority of the Category (Shrink C) instance - #42981

[Merged by Bors] - chore(CategoryTheory/EssentiallySmall): lower priority of the Category (Shrink C) instance#42981

dennj wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

dennj:shrink-preorder-category-prioritydennj/mathlib4:shrink-preorder-category-priorityCopy head branch name to clipboard