(deterministic) timeout

Stream: mathlib4

[Pietro Lavino]

I wrote some code that used to run just fine, and without changing anything I get: (deterministic) timeout at isDefEq, maximum number of heartbeats (200000) has been reached
use set_option maxHeartbeats <num> to set the limit
use set_option diagnostics true to get diagnostic information.

What can I do about this, this is a message I get even after trying to use apply? and use one of the proposed solutions, and a red line appears under the refine command with the error i just reported above

[Daniel Weber]

Is it possible one of the involved definitions had changed? Does increasing maxHeartbeats solve this?

[Kim Morrison]

The two set_option suggestions in the error message are what you need to look at! If it's possible for you to post code, or a link, someone may be able to give suggestions for improving your proof.