fix: log goalsAccomplished for theorems generated using elab (#15044)

[medovina]

This PR updates the definition elaborator so that a goalsAccomplished message will be logged for theorems that were generated using elab. That causes VS Code to display a double checkmark beside such theorems.

The fix works because when logGoalsAccomplishedSnapshotTask is called from elabMutualDef, the defsParsedSnap argument contains no definitions if we are in a context without a snapshot, which happens when theorems are generated using elab. That argument is used to determine whether an example is of type Prop, in which case a goalsAccomplished message should be logged for it. With this fix, if defsParsedSnap argument has no definitions then we will send a goalsAccomplished message for every example. As a consequence, if an example is generated using elab but is not of type Prop, it will get a checkmark in the IDE anyway. That is imperfect, however that situation should be be quite rare.

Closes #15044

[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 c155094f54eab345cca3da867dbd888a34fbf0d2 --onto c632a0a0e434a951cdcf61bb4da3344abadd5587. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-06 03:06:54)

[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 c155094f54eab345cca3da867dbd888a34fbf0d2 --onto 9de86005af5061b5ccf438d01134ee6d3ecea6b3. You can force reference manual CI using the force-manual-ci label. (2026-09-06 03:06:55)