nightly#155 adaptations for nightly-2026-01-05

Stream: nightly-testing

[github mathlib4 bot]

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

[Kevin Buzzard]

LGTM but am reluctant to hit merge because meta code is involved. Note that this is the first mathlib4-nightly-testing PR for quite some time which has passed CI so we're quite behind in terms of days (but it's only a very short PR).

[Damiano Testa]

The diff here looks like fallout from lean4#11893.

[Damiano Testa]

I'm a bit puzzled by docs#Lean.Meta.DiscTree.insertKeyValue, which does not seem to exist.

[Robin Arnez]

c.f. https://github.com/leanprover/lean4/pull/11884/changes#diff-6ea722cd64f21fadc8cec3a315801bbab0ad7c505d27d9e3c167429aae0b5406R164-R178
doc-gen isn't always up to date on lean nightly stuff

[Damiano Testa]

Thanks!

So then this accounts for all the metaprogramming changes!

[Kevin Buzzard]

Thanks Damiano! I've merged; it will be good to get nightly-testing up to date with lean.