mathlib

b8b8bf3e - refactor(category_theory/monoidal): prove coherence lemmas by coherence (#13406)

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