mathlib

0f4ac1bf - feat(category_theory/limits): product comparison simp lemmas (#5351)

feat(category_theory/limits): product comparison simp lemmas (#5351) This adds two new simp lemmas to reduce the prod comparison morphism and uses them to golf some proofs