Lean4
/-- Adding `@[reassoc]` to a lemma named `F` of shape `∀ .., f = g`, where `f g : X ⟶ Y` are
morphisms in some category, will create a new lemma named `F_assoc` of shape
`∀ .. {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h`
but with the conclusions simplified using the axioms for a category
(`Category.comp_id`, `Category.id_comp`, and `Category.assoc`).
So, for example, if the conclusion of `F` is `a ≫ b = g` then
the conclusion of `F_assoc` will be `a ≫ (b ≫ h) = g ≫ h` (note that `≫` reassociates
to the right so the brackets will not appear in the statement).
This attribute is useful for generating lemmas which the simplifier can use even on expressions
that are already right associated.
Note that if you want both the lemma and the reassociated lemma to be
`simp` lemmas, you should tag the lemma `@[reassoc (attr := simp)]`.
The variant `@[simp, reassoc]` on a lemma `F` will tag `F` with `@[simp]`,
but not `F_assoc` (this is sometimes useful).
This attribute also works for lemmas of shape `∀ .., f = g` where `f g : X ≅ Y` are
isomorphisms, provided that `Tactic.CategoryTheory.IsoReassoc` has been imported.
-/
@[attr_parser 1000]
public meta def reassoc : Lean.ParserDescr✝ :=
ParserDescr.node✝ `CategoryTheory.reassoc 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "reassoc" false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " (")
((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "attr" false✝))
(ParserDescr.symbol✝ " := "))
((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.parser✝ `Lean.Parser.Term.attrInstance) ","
(ParserDescr.symbol✝ ", ") Bool.false✝))
(ParserDescr.symbol✝ ")"))))
