chore: drop unnecessary synthInstance.maxHeartbeats increases

Author: Ruben-VandeVelde

FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean

@@ -60,8 +60,6 @@ theorem IsPrimitiveRoot.eq_one_mod_sub_of_pow {A : Type*} [CommRing A] [IsDomain
   obtain ⟨k, -, rfl⟩ := hζ.eq_pow_of_pow_eq_one hμ
   rw [map_pow, eq_one_mod_one_sub, one_pow]
 
-set_option synthInstance.maxHeartbeats 40000 in
--- needed for `AddMonoidHomClass (𝓞 K →+* 𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) ? ?`
 theorem aux {t} {l : 𝓞 K} {f : Fin t → ℤ} {μ : K} (hμ : IsPrimitiveRoot μ p)
     (h : ∑ x : Fin t, f x • (⟨μ, hμ.isIntegral (NeZero.pos p)⟩ : 𝓞 K) ^ (x : ℕ) = l) :
     algebraMap (𝓞 K) (𝓞 K ⧸ I) l = ∑ x : Fin t, (f x : 𝓞 K ⧸ I) := by
@@ -271,8 +269,6 @@ lemma unit_inv_conj_not_neg_zeta_runity_aux (u : (𝓞 K)ˣ) [Fact (p.Prime)] (h
     rw [this a]
   exact (aux hζ hζ hu).trans (aux hζ hζ.inv hu').symm
 
-set_option synthInstance.maxHeartbeats 40000 in
--- Needed for `AddMonoidHomClass (𝓞 K →+* 𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) ? ?`
 theorem unit_inv_conj_not_neg_zeta_runity (u : (𝓞 K)ˣ) (n : ℕ) [Fact (p.Prime)] (hp : 2 < p) :
     haveI := IsCyclotomicExtension.IsCMField K hp
     u * (unitsComplexConj K u)⁻¹ ≠ -hζ.unit' ^ n := by