Lean4
/-- Use the coherence theorem for monoidal categories to solve equations in a monoidal equation,
where the two sides only differ by replacing strings of monoidal structural morphisms
(that is, associators, unitors, and identities)
with different strings of structural morphisms 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 `pure_coherence`.
(If you have very large equations on which `coherence` is unexpectedly failing,
you may need to increase the typeclass search depth,
using e.g. `set_option synthInstance.maxSize 500`.)
-/
@[tactic_parser 1000]
public meta def coherence : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Coherence.coherence 1024 (ParserDescr.nonReservedSymbol✝ "coherence" false✝)
