Lean4
/-- Adding `@[to_app]` to a lemma named `F` of shape `∀ .., η = θ`, where `η θ : f ⟶ g` are 2-morphisms
in some bicategory, create a new lemma named `F_app`. This lemma is obtained by first specializing
the bicategory in which the equality is taking place to `Cat`, then applying `NatTrans.congr_app`
to obtain a proof of `∀ ... (X : Cat), η.app X = θ.app X`, and finally simplifying the conclusion
using some basic lemmas in the bicategory `Cat`:
`Cat.whiskerLeft_app`, `Cat.whiskerRight_app`, `Cat.id_app`, `Cat.comp_app` and `Cat.eqToHom_app`
So, for example, if the conclusion of `F` is `f ◁ η = θ` then the conclusion of `F_app` will be
`η.app (f.obj X) = θ.app X`.
This is useful for automatically generating lemmas that can be applied to expressions of 1-morphisms
in `Cat` which contain components of 2-morphisms.
Note that if you want both the lemma and the new lemma to be `simp` lemmas, you should tag the lemma
`@[to_app (attr := simp)]`. The variant `@[simp, to_app]` on a lemma `F` will tag `F` with
`@[simp]`, but not `F_app` (this is sometimes useful).
-/
@[attr_parser 1000]
public meta def to_app : Lean.ParserDescr✝ :=
ParserDescr.node✝ `CategoryTheory.to_app 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "to_app" 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✝ ")"))))
