heartbeats

leanprover-community · Nov 29, 2023 · a3c43d2 · a3c43d2
1 parent 390e7e2
commit a3c43d2
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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') ∧