fix: mathlib4 breakage from nightly-2026-09-11

[Kha]

Fixes the red master after the bump to nightly-2026-09-11 (run 34590361152). One commit, mathlib4 only.

mathlib4

Cause. The bump commit changes only lean-toolchain, yet Mathlib.FieldTheory.Galois.IsGaloisGroup stops compiling:

error: Mathlib/FieldTheory/Galois/IsGaloisGroup.lean:225:6: failed to synthesize
    Algebra K ↥(IsScalarTower.toAlgHom K F L).fieldRange
  (deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

It is a small drift. With Mathlib's leanOptions (maxSynthPendingDepth := 3), synthInstance.maxHeartbeats 21000 is already enough on nightly-2026-09-11. The adaptation branches for lean4#15090 (#64) and lean4#15066 (#59) hit the same error once their pr-releases were based on lean4 master past nightly-2026-09-10; pr-release-15090-0d7390f (based on the nightly-2026-09-10 commit) was fine and pr-release-15090-61a42c0 (based on lean4#15098) was not. That puts the cause among lean4#15001, #15093, #15060, #15048, #15107 and #15098. None of these obviously changes allocation counts inside instance synthesis, so I have not pinned it to one PR.

Fix. set_option synthInstance.maxHeartbeats 80000 in on IsGaloisGroup.of_isScalarTower, with the justifying comment the style linter asks for. This copies #64's hunk verbatim (the resulting blob is identical to the one on adaptation-15090), so merging #64 later stays clean. #59 raises the same limit to 40000 and will conflict on this line either way.

Verified locally on nightly-2026-09-11: lake build Mathlib Archive Counterexamples Wanted --wfail, lake test --iofail and lake lint all pass.

cslib

CI skipped it behind mathlib4, so it has not been built on this nightly. Verified locally, no change needed: lake build --wfail --iofail, lake test --wfail --iofail and lake lint all pass.

repl

Its lake test failed only as a knock-on: test.sh builds real Mathlib in test/Mathlib, which stopped at the same IsGaloisGroup error, and H20231110 then failed because Real was unavailable. No change needed. Verified locally: lake build and lake test pass with this fix.

Unfinished

Nothing.

[downstream-lean4]

Build report for fix: mathlib4 breakage from nightly-2026-09-11

Turned green:

Repo	Critical	Build	Test	Lint
mathlib4	✅	✅ in 233s	✅ in 48s	✅ in 97s
cslib		✅ in 34s	✅ in 8s	✅ in 3s
repl		✅ in 1s	✅ in 57s	⏭️

Stayed green

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 7s	✅ in 5s	⏭️
batteries	✅	✅ in 5s	✅ in 4s	✅ in 2s
import-graph	✅	✅ in 2s	✅ in 4s	⏭️
lean4-cli	✅	✅ in 1s	✅ in 0s	⏭️
plausible	✅	✅ in 1s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 3s	✅ in 1s	⏭️
quote4	✅	✅ in 2s	✅ in 1s	⏭️
reference-manual	✅	✅ in 76s	⏭️	⏭️
BibtexQuery		✅ in 3s	⏭️	⏭️
comparator		✅ in 2s	⏭️	⏭️
doc-gen4		✅ in 9s	⏭️	⏭️
illuminate		✅ in 4s	✅ in 10s	⏭️
lean4-unicode-basic		✅ in 2s	⏭️	⏭️
lean4export		✅ in 0s	✅ in 7s	⏭️
LeanSearchClient		✅ in 1s	✅ in 0s	⏭️
leansqlite		✅ in 7s	✅ in 15s	⏭️
nerodia		✅ in 3s	✅ in 21s	⏭️
verso		✅ in 91s	✅ in 169s	⏭️
verso-slides		✅ in 58s	✅ in 6s	⏭️
verso-web-components		✅ in 7s	⏭️	⏭️

View run