mathlib

4d0b6301 - feat(category_theory/bicategory/coherence_tactic): coherence tactic for bicategories (#13417)

feat(category_theory/bicategory/coherence_tactic): coherence tactic for bicategories (#13417) This PR extends the coherence tactic for monoidal categories #13125 to bicategories. The setup is the same as for monoidal case except for the following : we normalize 2-morphisms before running the coherence tactic. This normalization is achieved by the set of simp lemmas in `whisker_simps` defined in `coherence_tactic.lean`. As a test of the tactic in the real world, I have proved several properties of adjunction in bicategories in #13418. Unfortunately some proofs cause timeout, so it seems that we need to speed up the coherence tactic in the future. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>