mathlib

655b6171 - feat(category_theory/limits/preserves/shapes/products): preserve products (#4857)

feat(category_theory/limits/preserves/shapes/products): preserve products (#4857) A smaller part of #4716, for just products. This also renames the file `preserves/shapes.lean` to `preserves/shapes/products.lean`, since I want a similar API for other special shapes and it'd get too big otherwise. Of the declarations which were already present: `preserves_products_iso`, `preserves_products_iso_hom_π`, `map_lift_comp_preserves_products_iso_hom`, the first is still there but with weaker assumptions, and the other two are now provable by simp (under weaker assumptions again).