Klein 4 group PR relying on `decide := true` for `simp`

Stream: mathlib4

[Scott Morrison]

We've recently changed the default behaviour for simp so that it no longer calls decide. This is now regularly causing breakages on nightly-testing.

The most recent one is @Newell Jensen's PR #7937 which was just merged.

I've patched it on nightly-testing to change to calls to simp to simp (config := {decide := true}).

So two things:

• @Newell Jensen (or any one else) might want to have a look at this and decide if there is a better approach.
• All reviewers might keep an eye out for simp calls that are likely to be relying on decide, and either change them to simp (config := {decide := true}) for future proofing, or use a different approach.

[Newell Jensen]

Since this was recently changed I would have seen this if I had merged master or is this only on the nightly testing?

[Scott Morrison]

Unfortunately it is only nightly-testing, so no way for you to have foreseen this!

[Scott Morrison]

We're still learning how to manage nightly-testing, and I think today's lesson (this is just one of many examples of incoming PRs breaking nightly-testing) is that we are going to need to resynchronize more often.

[Scott Morrison]

I will probably cut a v4.3.0-rc2 version of Lean in the next couple of days.

[Newell Jensen]

What was the motivation to changesimp in this way? Was it so that usage of decide would be more atomic?

[Scott Morrison]

When simp fails to close a goal, sometimes it would launch very expensive attempts to decide the goal, that were not intended.