fix: `isDefEq` handling of delayed-assigned mvars when `withAssignableSyntheticOpaque` is `true`

[thorimur]

(In progress; fully experimental.)

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b9b4d8f41d93b9887d26a07746b283d582893c76 --onto 6719af350fde9339354f28d091458df39a4af9d4. (2024-02-23 03:38:54)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 87e7c666e23e676da70c02209a8f1979f467d45d --onto 5a32473f6695b44643ef81522e892c7d7b4be8d2. (2024-02-23 20:50:37)
• ✅ Mathlib branch lean-pr-testing-3473 has successfully built against this PR. (2024-03-08 00:39:27) View Log

[thorimur]

WIP