mathlib3

b55b1558 - feat(category_theory): a category with a small detecting set is well-powered