Commit 2020-11-07 08:45 655b6171

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).