Commit 2022-04-25 15:23 85075bcc
View on Github →refactor(category_theory/monoidal): rearrange simp lemmas to work better with coherence (#13409)
Change the direction of some simp lemma for monoidal categories, and remove some unused lemmas.
This PR is effectively a "no-op": no substantial changes to proofs. However, it should enable making coherence more powerful soon (following suggestions of @yuma-mizuno)!