mathlib3

d3c565d4 - feat(category_theory/monoidal): the monoidal coherence theorem (#7324)

feat(category_theory/monoidal): the monoidal coherence theorem (#7324) This PR contains a proof of the monoidal coherence theorem, stated in the following way: if `C` is any type, then the free monoidal category over `C` is a preorder. This should immediately imply the statement needed in the `coherence` branch.