diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
index b689c08051fcb..143530e7a97da 100644
--- 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.
 -/