perf: improve heuristic at isDefEq

[kim-em]

Adds a test case containing a minimization of a Mathlib slowdown from #3807, and a patch to isDefEq to fix the slowdown.

Prior to #3807, the declaration exists_algHom_adjoin_of_splits''' at the end of the file would take around 16,000 heartbeats. After #3807 it took around 210,000 heartbeats.

[kim-em]

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.

[kim-em]

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

[leanprover-community-mathlib4-bot]

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)