chore: audit and standardize grind E-graph internalization entry points

[kim-em]

This PR adds a preferred entry point preprocessAndInternalize for adding newly constructed
terms to the E-graph, and converts ad-hoc internalization sites to use it. This is preparatory
work for the grind simplification sets design, which requires every term in the E-graph to have
been through the full preprocessing pipeline.

A new function preprocessAndInternalize in Simp.lean composes preprocess and internalize
into a single call. Eight sites that previously used preprocessLight + internalize or bare
internalize are converted to use it, with proof adjustments where needed (e.g. composing
Simp.Result.proof? via mkEqTrans/mkHEqTrans).

Four sites are intentionally not converted, with explanations:

• Proj.lean: preprocessing would reduce proj_i (ctor ...) to the field value, breaking the
  congruence closure connection mechanism
• Cutsat/EqCnstr.lean (3 sites): terms are tightly coupled with the cutsat polynomial solver
  and mkVar registration

🤖 Prepared with Claude Code

[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 af2444a140d51e3c97247814204fef6821d2ba76 --onto 39c26fce1da321b24eaf949d0d7d028ba589e4e1. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-10 06:47:17)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase af2444a140d51e3c97247814204fef6821d2ba76 --onto 4cdc199f772977113bd6c1bf87a6c02b78d5c4d3. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-11 00:21:42)

[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 af2444a140d51e3c97247814204fef6821d2ba76 --onto 75d7f7eb227bc54dc6ea3d8ead090ee4180debaf. You can force reference manual CI using the force-manual-ci label. (2026-02-10 06:47:18)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase af2444a140d51e3c97247814204fef6821d2ba76 --onto 03dc334f73259e1bae0b8f2b80a39a82e1de3df6. You can force reference manual CI using the force-manual-ci label. (2026-02-11 00:21:43)