issue !4#18942: `@[simps]` is sometimes used to generate ...

Stream: triage

[Random Issue Bot]

Today I chose issue 18942 for discussion!

@[simps] is sometimes used to generate lemmas that we don't want @[simp] on
Created by @Kim Morrison (@kim-em) on 2024-11-12
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Violeta Hernández]

The comment on that issue means that this issue can be marked as resolved, am I correct?

[Mario Carneiro]

well, it's a tracking issue, so first the four references to it in mathlib should be cleaned up as appropriate