# Commit 2020-11-23 13:47 e8c8ce91

View on Github →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`

.