elementwise

Stream: mathlib4

[Joël Riou]

Thanks to @Kyle Miller and @Scott Morrison we now have the elementwise attribute. While porting CategoryTheory.Limits.Shapes.Types !4#2809 this attribute would sometimes produce ..._apply lemmas where the LHS is not simplified enough according to the simpNF linter (see https://github.com/leanprover-community/mathlib4/pull/2809/files#diff-bd1313dcddfed88eb46a2053178c60d4c91451e965a76da1672421458d44b87dR157-R179 ). In other cases, some rfl lemmas seem to be simplified too much because they just become True, see for example https://github.com/leanprover-community/mathlib4/pull/2809/files#diff-bd1313dcddfed88eb46a2053178c60d4c91451e965a76da1672421458d44b87dR468-R476

[Kyle Miller]

@Joël Riou Hopefully I haven't messed up what you're doing, but I pushed some changes to that branch to elementwise that hopefully address these issues. It now does a couple things:

1. It checks for when it generates True, which means it's something that simp almost definitely can do on its own without the lemma, so it suggests that you remove @[elementwise].
2. It by default applies the full simp set to the LHS and RHS of the generated lemma, which hopefully puts it into simp normal form (there's also a check that the result isn't trivial). To keep it from doing this step, there's @[elementwise nosimp].

[Kyle Miller]

I'll create a separate branch with a PR with these changes so that they can be reviewed independently.

[Kyle Miller]

Ok, these changes are at mathlib4#2956 if you feel like reverting my commit on mathlib4#2809.

[Joël Riou]

Thanks very much! It seems it works fine.