termReassoc_of%_ — Mathlib

Lean4
/-- `reassoc_of% t`, where `t` is
an equation `f = g` between morphisms `X ⟶ Y` in a category (possibly after a `∀` binder),
produce the equation `∀ {Z} (h : Y ⟶ Z), f ≫ h = g ≫ h`,
but with compositions fully right associated and identities removed.
This also works for equations between isomorphisms, provided that
`Tactic.CategoryTheory.IsoReassoc` has been imported.
-/
@[term_parser 1000]
public meta def «termReassoc_of%_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `CategoryTheory.«termReassoc_of%_» 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "reassoc_of% ") (ParserDescr.cat✝ `term 0))
Похожие утверждения