nightly#160 adaptations for nightly-2026-01-23

Stream: nightly-testing

[Kim Morrison]

chore: adaptations for nightly-2026-01-23 nightly#160 Please review this PR. At the next toolchain release this diff will land in 'master'.

[Johan Commelin]

Welcome back!

[Johan Commelin]

I left two comments.

[Kim Morrison]

Responded, thanks.

[Kim Morrison]

The changes that @Kevin Buzzard noticed (fixed by @Robin Arnez) were due to a regression in Lean, noted now as https://github.com/leanprover/lean4/issues/12136.

[Kim Morrison]

I've added #adaptation_note comments linking to https://github.com/leanprover/lean4/issues/12136 at all the sites in nightly-testing where simp perm lemma workarounds were needed. Commit: https://github.com/leanprover-community/mathlib4-nightly-testing/commit/85015ebb4d8

[Kim Morrison]

Updated: Fixed the #adaptation_note format (using proper doc comments now). New commit: https://github.com/leanprover-community/mathlib4-nightly-testing/commit/cb392c137f9

[Kevin Buzzard]

Many thanks for chasing this up!

[Kevin Buzzard]

Aah, the fact that it was done by AI will explain the error ;-)