perf: better isDefEq cache in the presence of metavariables

[JovanGerb]

This PR fixes the problem that unification in the presence of metavariables is often exponentially slow. This comes up every now and then in mathlib, and could get worse as mathlib continues to grow. This is implemented by handling the defEqTrans cache more carefully: we keep the cache as long as no metavariables are assigned.

To know when to invalidate the cache, we keep track of the number of assignments inside of a MetavarContext. We also store this number in Cache.defEqTrans, so if this number doesn't match the number in the current MetavarContext, we invalidate the cache. We also revert the transient cache in checkpointDefEq when needed (instead of emptying it).

Alternatively, to identify if the MetavarContext has progressed, it would be possible to define and use PersistentHashMap.size to find the number of assignments in the MetavarContext, but I didn't go for this option.

For this to work, in unification we need to wrap a checkpointDefEq around each branch that is backtracked on if it returns false. This was already meant to be like this, but some of these checkpoints were missing. In particular the addition in line 1932 (checkpointDefEq (isDefEqProjDelta t s i)) was needed to build mathlib. I added it in other places where I deemed this necessary.

The test file shows some examples improved by this fix.

The mathilb speedup from the fix is:

File	Instructions	%
build	-5685.569⬝10⁹	(-3.77%)
lint	-593.369⬝10⁹	(-8.44%)

Only one proof in mathlib had to be fixed. That particular failure was a unification that I think should not have been expected to work, and the fix was just a small change.

Zulip#lean4 > Exponential blowup in unification with metavariables @ 💬

closes #10414

[leanprover-community-bot]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-8883 build against this PR was cancelled. (2025-06-19 14:14:30) View Log
• ✅ Mathlib branch lean-pr-testing-8883 has successfully built against this PR. (2025-06-19 14:44:32) View Log
• ✅ Mathlib branch lean-pr-testing-8883 has successfully built against this PR. (2025-06-21 10:51:13) View Log
• 💥 Mathlib branch lean-pr-testing-8883 build failed against this PR. (2025-09-16 15:25:26) View Log
• ✅ Mathlib branch lean-pr-testing-8883 has successfully built against this PR. (2025-09-16 21:40:49) View Log
• 💥 Mathlib branch lean-pr-testing-8883 build failed against this PR. (2025-09-16 23:18:13) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-15 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-09-16 14:36:56)

[JovanGerb]

The mathlib failure is fixed in leanprover-community/mathlib4-nightly-testing#65