perf: add instance shortcut to remove heartbeat bump (#6410)

This removes a maxHeartbeats bump (the only one in the file).
leanprover-community · Aug 14, 2023 · c1776a3 · c1776a3
1 parent c54060b
commit c1776a3
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean
@@ -111,7 +111,9 @@ instance [NumberField K] : Fintype (torsion K) := by
   · rw [← h_ua]
     exact le_of_eq ((eq_iff_eq _ 1).mp ((mem_torsion K).mp h_tors) φ)
 
-set_option synthInstance.maxHeartbeats 30000 in
+-- a shortcut instance to stop the next instance from timing out
+instance [NumberField K] : Finite (torsion K) := inferInstance
+
 /-- The torsion subgroup is cylic. -/
 instance [NumberField K] : IsCyclic (torsion K) := subgroup_units_cyclic _