fixes for lean PR 12225

[JovanGerb]

---

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for 4198f04 against ae00d67 are in! @JovanGerb

• 🟥 main exited with code 1

No significant changes detected.

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for 2560e4a against e0bf30b are in! @JovanGerb

• build//instructions: +5.4T (+3.1%)

No significant changes detected.

[Garmelon]

Note that the bot doesn't yet use the mathlib significance thresholds

[JovanGerb]

I have encountered a couple of annoying problems when testing these adaptations

• I would have wanted to push to the autogenerated adaptation branch directly
• Since I don't have this right, I made a PR to the adaptation branch
• This doesn't run CI, so I have to build mathlib locally
• When running !bench on the PR, it compares the result with the adaptation branch, instead of the nightly-testing branch. So to get the right !bench result, I had to change the base branch of this PR.