Skip to content

Commit db41f4d

Browse files
mattrobballadomani
authored andcommitted
chore (RingTheory.Kaehler): reasonable heartbeat limits (#6178)
In light of #6141, we can change the heart beats to more representantive numbers. Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
1 parent 6d0663a commit db41f4d

1 file changed

Lines changed: 4 additions & 3 deletions

File tree

Mathlib/RingTheory/Kaehler.lean

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -391,7 +391,7 @@ theorem KaehlerDifferential.End_equiv_aux (f : S →ₐ[R] S ⊗ S ⧸ KaehlerDi
391391
set_option maxHeartbeats 700000 in
392392
-- Porting note: extra heartbeats are needed to infer the instance
393393
-- Module S { x // x ∈ Ideal.cotangentIdeal (ideal R S) }
394-
set_option synthInstance.maxHeartbeats 2000000 in
394+
set_option synthInstance.maxHeartbeats 200000 in
395395
-- This has type
396396
-- `Derivation R S (Ω[S⁄R]) ≃ₗ[R] Derivation R S (KaehlerDifferential.ideal R S).cotangentIdeal`
397397
-- But lean times-out if this is given explicitly.
@@ -412,8 +412,9 @@ def KaehlerDifferential.endEquivAuxEquiv :
412412
(Equiv.refl _).subtypeEquiv (KaehlerDifferential.End_equiv_aux R S)
413413
#align kaehler_differential.End_equiv_aux_equiv KaehlerDifferential.endEquivAuxEquiv
414414

415-
set_option maxHeartbeats 4100000 in
416-
set_option synthInstance.maxHeartbeats 4000000 in
415+
416+
set_option maxHeartbeats 1200000 in
417+
set_option synthInstance.maxHeartbeats 1000000 in
417418
/--
418419
The endomorphisms of `Ω[S⁄R]` corresponds to sections of the surjection `S ⊗[R] S ⧸ J ^ 2 →ₐ[R] S`,
419420
with `J` being the kernel of the multiplication map `S ⊗[R] S →ₐ[R] S`.

0 commit comments

Comments
 (0)