Investigate potential improvements to defeq caching

Around the time of investigating #2028, I also looked into the performance of the defeq cache and noticed a few potential issues that could be addressed in a future refinement of the cache (which this issue does not propose).

First, let's revisit the current definition of the cache, including potential improvements already mentioned there.
https://github.com/leanprover/lean4/blob/df8bf142f5fc9fbf53799f4b1dd5146961b4d18d/src/Lean/Meta/Basic.lean#L204-L208
https://github.com/leanprover/lean4/blob/df8bf142f5fc9fbf53799f4b1dd5146961b4d18d/src/Lean/Meta/Basic.lean#L1585-L1604

The last comment in particular mentions some basic limitations around caching across changed contexts and alternative approaches tried before. The first thing I noticed about this function is that the cache is reset in the beginning, but the old cache is not restored at the end, so it seems possible to accidentally reuse the cache across changed contexts after all and at the same time we lose cache data that possibly could be reused now that the original context is restored.

As the comment suggests, we call this function in isExprDefEq to ensure that different defeq calls use separate caches. Another interesting aspect however is that we call this same function in many nested steps as well: isDefEqEta,isDefEqEtaStruct,tryHeuristic,isDefEqApp. I don't know whether it is necessary to clear the cache in all these situations given that there is no direct change to the context, but in practice this should mean that we clear the cache at almost every step, so it would be great to make sure about this.

I also noticed calls of the opposite kind:
https://github.com/leanprover/lean4/blob/df8bf142f5fc9fbf53799f4b1dd5146961b4d18d/src/Lean/Meta/ExprDefEq.lean#L294
Here we do change the context but, because isExprDefEqAux is a direct recursive call that does not directly go through checkpointDefEq, could possibly end up with a stale cache (both when entering and exiting the call). Such issues may currently be masked by the frequent cache invalidation but could surface on future improvements to it.

As a final thought, before embarking on any optimization adventures of the defeq cache, it would be great to get a picture of the potential savings first. For example, we could as an experiment implement a second, not yet necessarily sound cache that we fill but do not actually use for computing the result, then measure the time spent on a miss in the current cache but not in the new cache as an upper limit of the saved time.

Start by reading the defeq cache definition and checkpointDefEq in src/Lean/Meta/Basic.lean, then trace the listed callers such as isExprDefEq and isDefEqApp. Inspect the recursive context change around isExprDefEqAux in src/Lean/Meta/ExprDefEq.lean. Done means establishing safe cache behavior across these boundaries and measuring the potential savings before proposing an optimization.