Commit 2022-04-24 04:20 b8b8bf3e

refactor(category_theory/monoidal): prove coherence lemmas by coherence (#13406) Now that we have a basic monoidal coherence tactic, we can replace some boring proofs of particular coherence lemmas with by coherence. I've also simply deleted a few lemmas which are not actually used elsewhere in mathlib, and can be proved by coherence.