refactor: make simpH proof-producing

Open nomeata opened this issue 1 month ago • 2 comments

This PR makes simpH, used in the match equation generator, produce a proof term. This is in preparation for a bigger refactoring.

Dec 08 '25 15:12 nomeata

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-05 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. (2025-12-08 16:50:37)

Dec 08 '25 16:12 leanprover-bot

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-11553 has successfully built against this PR. (2025-12-08 17:53:24) View Log
✅ Mathlib branch lean-pr-testing-11553 has successfully built against this PR. (2025-12-08 23:17:25) View Log

Dec 08 '25 17:12 leanprover-community-bot