Curiously, deleting setOf in both

def range (f : ι → α) : Set α := setOf fun x => ∃ y, f y = x

and

def image (f : α → β) (s : Set α) : Set β := setOf fun b => ∃ a ∈ s, f a = b

reduces the heartbeat count to around 80,000.

These are the outputs of

set_option trace.Meta.isDefEq true in
exact (congrFun (congrArg (fun g : L' →ₐ[F] K => (g : L' → K)) hφ) _).trans (congrArg f <| AlgEquiv.symm_apply_apply _ _)

(i.e. the step that is timing out) both before and after #3807. Be warned that after.txt is about 7gb uncompressed....
before.txt.gz
after.txt.gz

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-04-05 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-04-06 07:48:20)
• ❗ Std CI can not be attempted yet, as the nightly-testing-2024-04-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-04-21 21:29:45)