fix: recognize opaque constants of unit-like types as definitionally equal

[kernelpanic888]

This PR allows rfl to prove equality between distinct opaque constants whose common type is unit-like, fixing #14348.

The definitional equality checker now falls back to its existing unit-like check only when two constant names differ, preserving the fast path for identical constants. A regression test covers two opaque Unit constants.

Tests

• Clean stage1 build
• tests/with_stage1_test_env.sh tests/elab/run_test.sh 14348.lean

Changelog

• changelog-language

AI assistance

AI assistance was used to locate the diagnosed control-flow branch and draft the minimal patch and regression test. I manually reviewed the change and verified the clean build and focused test.

[kernelpanic888]

The syntax error is fixed in commit 0ebf6be; distinct constants now fall through to the existing unit-like check while identical constants keep the universe-level fast path. The PR body check also requires a changelog label, but fork contributors cannot add upstream labels. Maintainers: please add changelog-language (or the category you prefer).

[kernelpanic888]

The focused 14348 regression passed in the refreshed CI. The remaining failure was trace-only: distinct non-unit constants were falling through the general expensive path and adding isDefEq.onFailure trace entries. Commit 2fdb446267 now sends distinct constants directly to isDefEqUnitLike; non-unit-like types return false immediately, preserving the previous trace/control-flow boundary.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-07-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-30 20:43:39)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 58774429865502f05c63239266aac30ef1e91ef7 --onto c632a0a0e434a951cdcf61bb4da3344abadd5587. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-04 00:36:05)

[leanprover-bot]

Reference manual CI status:

• 🟡 Reference manual branch lean-pr-testing-14550 build against this PR didn't complete normally. (2026-07-30 20:50:39) View Log
• ✅ Reference manual branch lean-pr-testing-14550 has successfully built against this PR. (2026-07-30 20:51:05) View Log
• ✅ Reference manual branch lean-pr-testing-14550 has successfully built against this PR. (2026-07-30 21:16:55) View Log
• 🟡 Reference manual branch lean-pr-testing-14550 build against this PR didn't complete normally. (2026-07-30 21:17:13) View Log
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 58774429865502f05c63239266aac30ef1e91ef7 --onto 19c79593c47bb8dd3371327c08fc80775d8488af. You can force reference manual CI using the force-manual-ci label. (2026-09-04 00:36:06)

[kernelpanic888]

changelog-language