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

The elementwise attribute

The elementwise attribute can be applied to a lemma

@[elementwise]
lemma some_lemma {C : Type*} [category C] {X Y : C} (f g : X ⟶ Y) : f = g := ...

and produce

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.