mathlib

b583055c - feat(category_theory): a category with a small detecting set is well-powered (#15238)