fix: vcgen [f] unfolding of definitions by root match

[sgraf812]

This PR makes vcgen [f] handle a definition f whose body is a match on its arguments like simp [f] does. A call with an opaque discriminant now rewrites with the unfold theorem f.eq_def and splits the exposed match, instead of reporting a missing spec. Wildcard-row equations guarded by an overlap hypothesis are no longer used as specs; applying one committed the goal to the wildcard alternative and left the overlap hypothesis as an unprovable verification condition.

The spec database now interprets a simp set the way simp itself does: equations arrive as simp theorem entries, and a toUnfold entry contributes f.eq_def at priority 0 as the spec counterpart of delta unfolding, guarded by isRecursiveDefinition where simp relies on smart unfolding at rewrite time. The attribute [spec] f path derives its entries from mkSimpEntryOfDeclToUnfold as well, and mkSpecTheoremFromSimpDecl? rejects overlap-guarded equations, which vcgen cannot apply the way simp does because spec application emits hypotheses as verification conditions rather than attempting to discharge them.

[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 78745e26da2102fd51d04cf64b550b6746a06645 --onto a4b639c5a1e545677b36b09a4770b7b559df805b. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-17 09:38:47)

[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 78745e26da2102fd51d04cf64b550b6746a06645 --onto a4b639c5a1e545677b36b09a4770b7b559df805b. You can force reference manual CI using the force-manual-ci label. (2026-07-17 09:38:48)

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for dd239ef against 78745e2 are in. No significant results found. @sgraf812

• 🟥 build//instructions: +1.8G (+0.02%)

Medium changes (1✅)

• ✅ elab/bv_decide_mod//maxrss: -194MiB (-9.46%)

Small changes (2✅, 1🟥)

• 🟥 build/module/Lean.Elab.Tactic.Do.Attr//instructions: +274.8M (+3.85%) (reduced significance based on *//lines)
• ✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.SpecDB//instructions: -112.5M (-3.92%) (reduced significance based on *//lines)
• ✅ build/module/Std.Data.Iterators.Lemmas.Equivalence.Basic//instructions: -68.6M (-3.22%) (reduced significance based on absolute threshold)