Commit 2020-11-23 13:47 e8c8ce91

chore(category_theory/limits): move product isomorphisms (#5057) This PR moves some constructions and lemmas from monoidal/of_has_finite_products (back) to limits/shapes/binary_products. This reverts some changes made in https://github.com/leanprover-community/mathlib/commit/18246ac427c62348e7ff854965998cd9878c7692#diff-95871ea16bec862dfc4359f812b624a7a98e87b8c31c034e8a6e792332edb646. In particular, the purpose of that PR was to minimise imports in particular relating to finite_limits, but moving these particular definitions back doesn't make the imports any worse in that sense - other than that binary_products now imports terminal which I think doesn't make the import graph much worse. On the other hand, these definitions are useful outside of the context of monoidal categories so I think they do genuinely belong in limits/. I also changed some proofs from tidy to simp or a term-mode proof, and removed a simp attribute from a lemma which was already provable by simp.