mathlib

23dbb4cf - feat(tactic/elementwise): autogenerate lemmas in concrete categories (#6941)

feat(tactic/elementwise): autogenerate lemmas in concrete categories (#6941) # The `elementwise` attribute The `elementwise` attribute can be applied to a lemma ```lean @[elementwise] lemma some_lemma {C : Type*} [category C] {X Y : C} (f g : X ⟶ Y) : f = g := ... ``` and produce ```lean lemma some_lemma_apply {C : Type*} [category C] [concrete_category C] {X Y : C} (f g : X ⟶ Y) (x : X) : f x = g x := ... ``` (Here `X` is being coerced to a type via `concrete_category.has_coe_to_sort` and `f` and `g` are being coerced to functions via `concrete_category.has_coe_to_fun`.) 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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>