From 3664a432e43f632b846c0a4477533bce5990470e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 11 Sep 2026 11:35:14 +0000 Subject: [PATCH] fix: mathlib4 breakage from nightly-2026-09-11 The bump from `nightly-2026-09-10` to `nightly-2026-09-11` (the bump commit changes only `lean-toolchain`) pushes the `Algebra K (IsScalarTower.toAlgHom K F L).fieldRange` instance search in `IsGaloisGroup.of_isScalarTower` just past the default `synthInstance.maxHeartbeats` of 20000; with Mathlib's `leanOptions` 21000 already suffices. The same failure appeared on the lean4#15090 and lean4#15066 pr-releases once they were based on lean4 master after nightly-2026-09-10, and both adaptation branches raise the limit. Mirror the hunk of adaptation-15090 (#64) verbatim, so that the file ends up byte-identical to that branch and its eventual merge stays clean. --- mathlib4/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/mathlib4/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean b/mathlib4/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean index f9c0bad6a..dae6ea0e7 100644 --- a/mathlib4/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean +++ b/mathlib4/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean @@ -202,6 +202,9 @@ instance intermediateField [Finite G] [hGKL : IsGaloisGroup G K L] : have := hGKL.isGalois .of_mulEquiv_algEquiv e fun _ _ ↦ rfl +set_option synthInstance.maxHeartbeats 80000 in +-- The `Algebra K (IsScalarTower.toAlgHom K F L).fieldRange` instance in the proof needs more +-- than the default limit. attribute [local instance] FractionRing.liftAlgebra in /-- If `G` is a finite Galois group for `B / R` and `R ⊆ A ⊆ B` is a tower of commutative domains with `A` integrally closed, then the fixing subgroup of the image of `A` in `B` is a Galois group