fix: allow restoring erased simp attributes

[sankalpsthakur]

This PR lets an explicit attribute [simp] restore a theorem or definition after attribute [-simp] erased it in the current environment.

Simp erasure records an origin in a separate tombstone set. Re-adding the corresponding simp entry populated the theorem data again but left that tombstone in place, so the simplifier continued to ignore it.

Clear the matching tombstone when the attribute handler explicitly re-adds a proposition, definition, or generated equation theorem. The existing erase-simp test now includes the reproducer from #5868.

Closes #5868

Validation

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

AI assistance

AI tools assisted with issue triage, extension-state analysis, implementation, and regression preparation. I reviewed the tombstone semantics, reverse simp origins, definition equation entries, and final 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 07:16:37)
• ✅ Mathlib branch lean-pr-testing-14657 has successfully built against this PR. (2026-08-02 19:42:49) View Log
• ✅ Mathlib branch lean-pr-testing-14657 has successfully built against this PR. (2026-08-04 02:58:25) View Log

[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 07:16:39)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-02 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-02 18:47:56)