fix: variable must execute pending tactics and elaboration problems

[leodemoura]

closes #2226
closes #3214

[leodemoura]

@semorrison This PR may affect Mathlib. If there are too many issues, we should just skip this PR and fix the issues above when we address RFC #2452

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4370 build failed against this PR. (2024-06-06 01:50:20) View Log
• 💥 Mathlib branch lean-pr-testing-4370 build failed against this PR. (2024-06-06 02:51:56) View Log
• ✅ Mathlib branch lean-pr-testing-4370 has successfully built against this PR. (2024-06-06 06:02:59) View Log

[kim-em]

@leodemoura, the fallout in Mathlib is manageable. The only change is that we can no longer change the explicitness of a variable, and in the same line introduce a new variable that depends on it.

(I'm not sure if that is an intended or avoidable effect of this PR!)

[kim-em]

Mathlib should build now. Diff is at leanprover-community/mathlib4@026f1b9 for reference.

[eric-wieser]

The only change is that we can no longer change the explicitness of a variable, and in the same line introduce a new variable that depends on it.

This was often a footgun in mathlib anyway, as sometimes it resulted in duplicate hypotheses.

[leodemoura]

The only change is that we can no longer change the explicitness of a variable, and in the same line introduce a new variable that depends on it.

This was often a footgun in mathlib anyway, as sometimes it resulted in duplicate hypotheses.

Thanks for feedback. So, I will go ahead and merge the PR.