pure_coherence — Mathlib

Lean4
/-- `pure_coherence` uses the coherence theorem for monoidal categories to prove the goal.
It can prove any equality made up only of associators, unitors, and identities.
```lean
example {C : Type} [Category C] [MonoidalCategory C] :
  (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom := by
  pure_coherence
```

Users will typically just use the `coherence` tactic,
which can also cope with identities 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`
-/
@[tactic_parser 1000]
public meta def pure_coherence : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.Coherence.pure_coherence 1024
    (ParserDescr.nonReservedSymbol✝ "pure_coherence" false✝)
Похожие утверждения