Lean4
/-- `elementwise_of% h`, where `h` is a proof of an equation `f = g` between
morphisms `X ⟶ Y` in a concrete category (possibly after a `∀` binder),
produces a proof of equation `∀ (x : X), f x = g x`, but with compositions fully
right associated and identities removed.
A typical example is using `elementwise_of%` to dynamically generate rewrite lemmas:
```lean
example (M N K : MonCat) (f : M ⟶ N) (g : N ⟶ K) (h : M ⟶ K) (w : f ≫ g = h) (m : M) :
g (f m) = h m := by rw [elementwise_of% w]
```
In this case, `elementwise_of% w` generates the lemma `∀ (x : M), f (g x) = h x`.
Like the `@[elementwise]` attribute, `elementwise_of%` inserts a `HasForget`
instance argument if it can't synthesize a relevant `HasForget` instance.
(Technical note: The forgetful functor's universe variable is instantiated with a
fresh level metavariable in this case.)
One difference between `elementwise_of%` and `@[elementwise]` is that `@[elementwise]` by
default applies `simp` to both sides of the generated lemma to get something that is in simp
normal form. `elementwise_of%` does not do this.
-/
@[term_parser 1000]
public meta def «termElementwise_of%_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Tactic.Elementwise.«termElementwise_of%_» 1022
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "elementwise_of% ") (ParserDescr.cat✝ `term 0))
