fix: grind congruence-table invariant for lazy ite branches

[leodemoura]

This PR fixes a grind congruence-table invariant violation that could panic
when an ite branch was internalized lazily (after the condition became True
or False) and that branch's equivalence class was later merged with another.

Internalize.lean has a special case for ite that internalizes only the
condition; the then/else branches are skipped and only internalized later
on demand by propagateIte. The on-demand path (applyCongrFun) called
internalize for the branch but never called registerParent to add the
parent ite to the branch's parent set in the e-graph. Subsequent merges of
the branch's equivalence class then skipped re-hashing the ite in the
congruence table, leaving an orphan entry whose congr chain no longer matched
the table's representative.

The fix adds the explicit registerParent e rhs that the standard
for arg in args loop in Internalize.lean would have made for an ordinary
application argument; we are simply mirroring that pattern lazily. The same
helper is reused by propagateDIte, but with parent registration disabled
(controlled by a new ite : Bool parameter): for dite the rhs propagated
upwards is a constructed reduction (built via mkApp from e's children,
possibly post-preprocess), not a structural argument of e, so registering
e as its parent would be incorrect. The lambda branches of a dite are
already eagerly internalized as parents of e by Internalize.lean, so this
case does not need the fix.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-03 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-05-03 15:31:31)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 1b23b051f369dfedddd5b255c7e9bedbf5953eff --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-05-03 18:08:07)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-13624 has successfully built against this PR. (2026-05-03 16:27:19) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1b23b051f369dfedddd5b255c7e9bedbf5953eff --onto fe3c7394fd3acb1faecf6fc26f267eb22058fe66. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-03 18:08:06)