breakage on `bump/v4.8.0` from #11333

Stream: nightly-testing

[Kim Morrison]

@Damiano Testa, one of your replacements of useless tactics in #11333 unfortunately doesn't work on the bump/v4.8.0 branch, and now that I've merged master into it, it is broken.

This is https://github.com/leanprover-community/mathlib4/pull/11333/files#diff-d47323ee8b4b2321052b4be93715f8b2f3f840f76ec441d8bf75c834b8665b32

Can we just revert that chunk? It's already been reverted on nightly-testing.

[Kim Morrison]

Or come up with a shorter proof that will still work on nightly-testing.

[Damiano Testa]

Sure, feel free to undo the whole batch: I won't have time to debug until tomorrow, and re-running the linter on the bump should be easy anyway.

[Damiano Testa]

(I've also observed more useless tactics creeping in on master already anyway.)

[Kim Morrison]

I've just undone that one, directly on bump/v4.8.0.

[Damiano Testa]

The bump/v4.8.0 branch has two broken (consecutive!) simp? says. Is it ok if I simply push a fix to them? (The fix is just replacing the old outcome with the new one.)

[Ruben Van de Velde]

Yes please

[Damiano Testa]

It turns out that I cannot:

remote: error: GH006: Protected branch update failed for refs/heads/bump/v4.8.0.
remote: error: You're not authorized to push to this branch. Visit https://docs.github.com/articles/about-protected-branches/ for more information.
To github.com:leanprover-community/mathlib4.git
 ! [remote rejected]       bump/v4.8.0 -> bump/v4.8.0 (protected branch hook declined)
error: failed to push some refs to 'github.com:leanprover-community/mathlib4.git'

[Damiano Testa]

However, you can

git cherry-pick 4cb6efad547cd787fa732a27fbb1414163553eed
git cherry-pick d9028721cad8abb615a4d0f520f87e2b4e947e9c

after you fetch a current version of mathlib.

(They come one at a time...)

[Damiano Testa]

CI is passing for me locally with the two cherry-picked patches above.

[Damiano Testa]

Shake is unhappy, though.

[Ruben Van de Velde]

Oh, sorry, I misread the branch name

[Damiano Testa]

No problem, the two patches should work for whoever has write access. I can also produce the patch for shake, if it is helpful.

[Ruben Van de Velde]

You can create a PR into the bump/ branch

[Damiano Testa]

Ah, true! I'll do that.

[Damiano Testa]

Hopefully this will build! #11533