Is this a good simp lemma?

Stream: general

[Gabriel Ebner]

We have a lot of simp lemmas of the following form:

@[simp] lemma foo : bar = baz := by simp

Is this ever useful? Were these intentional?

[Mario Carneiro]

they are shortcut rules

[Mario Carneiro]

I know why you are asking, but since it's confluent it doesn't matter if the lemma triggers or not

[Mario Carneiro]

maybe just nolint them

[Gabriel Ebner]

they are shortcut rules

So I guess I'll just rewrite the linter and check that (i.e. that they are indeed used preferentially). Putting nolint is not really an option since they are lots of these lemmas.