From a3c43d202a9bd2f818473bbb068cb5a7bdcf81b3 Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Wed, 29 Nov 2023 19:36:55 +0000
Subject: [PATCH] heartbeats

---
 FltRegular/CaseII/InductionStep.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/FltRegular/CaseII/InductionStep.lean b/FltRegular/CaseII/InductionStep.lean
index 9257a083..dbe2ccfe 100644
--- a/FltRegular/CaseII/InductionStep.lean
+++ b/FltRegular/CaseII/InductionStep.lean
@@ -452,6 +452,7 @@ lemma stuff (η₁) (hη₁ : η₁ ≠ η₀) (η₂) (hη₂ : η₂ ≠ η₀
   congr 1
   ring
 
+set_option maxHeartbeats 400000 in
 lemma exists_solution :
   ∃ (x' y' z' : 𝓞 K) (ε₁ ε₂ ε₃ : (𝓞 K)ˣ),
     ¬((hζ.unit' : 𝓞 K) - 1 ∣ x') ∧ ¬((hζ.unit' : 𝓞 K) - 1 ∣ y') ∧ ¬((hζ.unit' : 𝓞 K) - 1 ∣ z') ∧