simp on Compares downstream effects

Stream: mathlib4

[Yakov Pechersky]

In mathlib4#569, the simp linter complains (https://github.com/leanprover-community/mathlib4/actions/runs/3493270005/jobs/5847924039) because the Compare definition simplifies on the LHS, thus toDual_compares_toDual : Compares o (toDual a) (toDual b) ↔ Compares o b a simplifies partially. Apparently, this is not an issue for the mathlib3 simp linter. Should we untag Compares with [simp]?

[Mario Carneiro]

this is another lean 4 change: nonrecursive definitions marked as @[simp] and defined by the equation compiler eagerly unfold (into a match expression), which is usually undesirable and not what lean 3 simp did

[Mario Carneiro]

(this should be mentioned on the wiki and/or fixed in core)

[Mario Carneiro]

the fix is to not mark it as simp and instead mark the equations (e.g. compares_lt, compares_eq, ..) as simp

[Adam Topaz]

Can simps be modified so that a @[simps] on such a definition would mark the equations with simp?