mathlib

85075bcc - refactor(category_theory/monoidal): rearrange simp lemmas to work better with coherence (#13409)

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)! Co-authored-by: Scott Morrison <scott.morrison@gmail.com>