fix: assign proof-valued inferred instances

[sankalpsthakur]

This PR ensures MVarId.inferInstance actually assigns the goal when the synthesized instance is proof-valued.

For propositions, proof irrelevance can make isDefEq (mkMVar mvarId) synthVal succeed without assigning mvarId. inferInstance then returned successfully, and a caller that removed the goal produced a declaration containing an unresolved metavariable.

After successful definitional equality, explicitly assign the synthesized value only when the goal remains unassigned. The regression is the concrete custom-tactic reproducer from #2054.

Closes #2054

Validation

• Added tests/elab/issue2054.lean
• Exact PR-history search found no competing implementation
• Full Lean CI is the authoritative validation

AI assistance

AI tools assisted with issue triage, source inspection, implementation, and regression preparation. I reviewed the proof-irrelevance path and final two-line production diff.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 23d17351ab630c393aadb7f8c97ef9b8ee633cdb --onto 5b8d06c1764fa367a1e27b3e89f64667eac425af. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-02 06:55:50)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 23d17351ab630c393aadb7f8c97ef9b8ee633cdb --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-02 06:55:51)