Commit 2024-07-25 07:08 7eaaae5c

chore(Tactic/CategoryTheory/Coherence): import non-meta coherence theorem (#15067) The definition of the coherence tactic do not require the non-meta coherence theorem, but it implicitly assumes the theorem when running the meta program. It would be confusing if the coherence tactic failed because you did import Mathlib.Tactic.CategoryTheory.Coherence but forgot to import Mathlib.CategoryTheory.Monoidal.Free.Coherence. This PR makes the first file import the second one (and similarly for the bicategory version).