mathlib

b26fc59f - feat(category_theory/limits/shapes/products): pi comparison morphism (#4855)