[Merged by Bors] - feat(tactic/elementwise): autogenerate lemmas in concrete categories

[semorrison]

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.

---

This doesn't immediately remove many lemmas, but I think the real situation is that we have wanted many lemmas of this form, but everyone immediately sees that humans shouldn't have to write them, and stops working on whatever needed the lemmas. :-)

For now I've reduced the main culprit file to a short stub with just an attribute ... line. I will probably update this PR to delete that file, distributing those attributes around to the original declarations.

I don't intend to add lots of @[elementwise] attributes in this PR; they can be added as needed later.

[b-mehta]

I can't comment on the contents of the meta code here, but this is definitely a good tactic to have! Do you think the autogenerated lemmas in limits/concrete should be marked simp again? reassoc also has reassoc_of - I don't know the internals of it but it can be useful in the case where there's a local hypothesis which I'd like to reassociate. I imagine there might be cases where you want something similar here: is something like elementwise_of doable (outside this PR if necessary).
In the zulip thread you mentioned that certain dsimp lemmas are applied to the resulting lemma, I think this should be mentioned in one of the docstrings here

[gebner]

I think the real situation is that we have wanted many lemmas of this form

At first glance, some_lemma_apply seems to be less general and hence less useful than some_lemma (e.g. it looks like you could always write simp [some_lemma] instead of simp [some_lemma_apply]). Can you explain why we nevertheless want to have some_lemma_apply?

[semorrison]

I think the real situation is that we have wanted many lemmas of this form

At first glance, some_lemma_apply seems to be less general and hence less useful than some_lemma (e.g. it looks like you could always write simp [some_lemma] instead of simp [some_lemma_apply]). Can you explain why we nevertheless want to have some_lemma_apply?

Ah -- the point, which I should explain in the docs, is that elementwise simplifies the form of the statement using concrete_category.coe_id : ((𝟙 X) : X → X) x = x and concrete_category.coe_comp : (f ≫ g) x = g (f x).

This difference is all that prevents you from using the original lemma.

EDIT: I've updated the doc-strings so the example indicates this in action.

[semorrison]

I imagine there might be cases where you want something similar here: is something like elementwise_of doable.

It's certainly doable, but it's also just concrete_category.congr_hom w. I agree though it would be easier to find if there was something that matched the attribute.

[semorrison]

@b-mehta, what do you think about names? I was thinking about just @[concrete] instead of @[elementwise].

Similarly, should we think about the _apply prefix? I think I'm happy with that one.

[b-mehta]

I imagine there might be cases where you want something similar here: is something like elementwise_of doable.

It's certainly doable, but it's also just concrete_category.congr_hom w. I agree though it would be easier to find if there was something that matched the attribute.

This is true, but reassoc_of is really nice for rewriting while concrete_category.congr_hom (probably?) doesn't have good syntactic properties - hence the dsimps you mention in this lemma.

@b-mehta, what do you think about names? I was thinking about just @[concrete] instead of @[elementwise].

I think I (weakly) prefer elementwise to concrete, but I'd be happy with either - concrete is more concise but I think elementwise is clearer?

Similarly, should we think about the _apply prefix? I think I'm happy with that one.

Also happy with this.

[semorrison]

Okay! I will leave the names as is. I have added elementwise_of (an expression) and elementwise a tactic, just as for reassoc.

[gebner]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests