Lean4
/-- The `elementwise` attribute can be added to a lemma proving an equation of morphisms, and it
creates a new lemma for a `HasForget` giving an equation with those morphisms applied
to some value.
Syntax examples:
- `@[elementwise]`
- `@[elementwise nosimp]` to not use `simp` on both sides of the generated lemma
- `@[elementwise (attr := simp)]` to apply the `simp` attribute to both the generated lemma and
the original lemma.
Example application of `elementwise`:
```lean
@[elementwise]
lemma some_lemma {C : Type*} [Category C]
{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : X ⟶ Z) (w : ...) : f ≫ g = h := ...
```
produces
```lean
lemma some_lemma_apply {C : Type*} [Category C]
{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : X ⟶ Z) (w : ...)
[HasForget C] (x : X) : g (f x) = h x := ...
```
Here `X` is being coerced to a type via `CategoryTheory.HasForget.hasCoeToSort` and
`f`, `g`, and `h` are being coerced to functions via `CategoryTheory.HasForget.hasCoeToFun`.
Further, we simplify the type using `CategoryTheory.coe_id : ((𝟙 X) : X → X) x = x` and
`CategoryTheory.coe_comp : (f ≫ g) x = g (f x)`,
replacing morphism composition with function composition.
The `[HasForget C]` argument will be omitted if it is possible to synthesize an instance.
The name of the produced lemma can be specified with `@[elementwise other_lemma_name]`.
If `simp` is added first, the generated lemma will also have the `simp` attribute.
-/
@[attr_parser 1000]
public meta def elementwise : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Tactic.Elementwise.elementwise 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "elementwise" false✝)
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ " nosimp")))
(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✝ ")"))))
