Commit 2023-06-28 07:29 208982a6

feat: don't re-elaborate terms in set (#5386) Fix the set tactic to not time out when dealing with slow to elaborate terms and many local hypotheses. The root cause of this is that the rewrite [blah] at * tactic causes blah to be elaborated again and again for each local hypothesis, this is possibly a core issue that should be fixed separately, but in set we have the elaborated term already so we can just use it. We also add some functionality to simply test / demonstrate failures when elaboration takes too long, namely sleepAtLeastHeartbeats and a sleep_heartbeats tactic. @urkud was facing some slow running set's in https://github.com/leanprover-community/mathlib4/pull/4912, see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Timeout.20in.20.60set.20.2E.2E.20with.60/near/367958828 that this issue was minimized from and should fix. Some other linter failures show up due to changes to the set internals so fix these too.