mathlib3

fdbcab6a - feat(category_theory/limits): the product comparison natural transformation (#5621)