fix build for leanprover/lean4#6577

leanprover-community · Jan 8, 2025 · aa3ade5 · aa3ade5
1 parent 8100f74
commit aa3ade5
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
@@ -174,6 +174,7 @@ theorem f_invApp_f_app (i j k : D.J) (U : Opens (D.V (i, j)).carrier) :
   rfl
 
 set_option backward.isDefEq.lazyWhnfCore false in -- See https://github.com/leanprover-community/mathlib4/issues/12534
+set_option maxHeartbeats 400000 in
 /-- We can prove the `eq` along with the lemma. Thus this is bundled together here, and the
 lemma itself is separated below.
 -/