fix: handle delayed-assigned mvars in `isDefEq` safely

[thorimur]

Currently, unknown fvars can be introduced during isDefEq when synthetic opaque metavariables are assignable and appear in a delayed assignment. Specifically, if ?m.23 is delayed-assigned to ?a, we currently replace ?m.23 as bs with ?a bs. However, if the type of ?a depends on the new fvars in its context, we've now introduced unknown fvars to isDefEq. Notably, this happens when elaborating expressions like fun x => ?a which leave the type of ?a unspecified (and therefore dependent on x via another delayed-assigned mvar).

This PR checks that either the context of ?a is compatible with the local context, or attempts to clear the new fvars from ?a's context if ?a's context is strictly larger than the current one. Otherwise, isDefEq now fails.

---

Closes #3393

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-3637 build failed against this PR. (2024-03-08 19:54:27) View Log
• 💥 Mathlib branch lean-pr-testing-3637 build failed against this PR. (2024-03-10 00:15:48) View Log

[kim-em]

It looks like the Mathlib failure is genuinely caused by this PR, right?

[thorimur]

Yes, I believe this one's for real. :) It introduces the possibility of isDefEq failing where it otherwise wouldn't. Contrast with #3473 (an alternate more experimental approach to the same problem) which built mathlib around the same time.