feat(category_theory/monoidal): coherence tactic (#13125)
This is an alternative to #12697 (although this one does not handle bicategories!)
From the docstring:
```
Use the coherence theorem for monoidal categories to solve equations in a monoidal equation,
where the two sides only differ by replacing strings of "structural" morphisms with
different strings with the same source and target.
That is, `coherence` can handle goals of the form
`a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'`
where `a = a'`, `b = b'`, and `c = c'` can be proved using `coherence1`.
```
This PR additionally provides a "composition up to unitors+associators" operation, so you can write
```
example {U V W X Y : C} (f : U ⟶ V ⊗ (W ⊗ X)) (g : (V ⊗ W) ⊗ X ⟶ Y) : U ⟶ Y := f ⊗≫ g
```
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: yuma-mizuno <mizuno.y.aj@gmail.com>
