doc: clarify Expr.forEachWhere semantics

[sankalpsthakur]

This PR documents the two behavioral differences between Expr.forEachWhere and Expr.forEach that matter to callers.

Matching subterms are deduplicated by structural equality, so the callback runs at most once for each distinct matching expression even when it occurs multiple times. The traversal also carries pointer and hash-set caches, which can be beneficial for selective predicates or expensive callbacks but can cost more than forEach when most subterms match.

The public stopWhenVisited description is also made precise: descent stops when the callback is invoked for a matching subterm.

Closes #2511

Validation

• Documentation-only source change
• The description follows the visited and checked state used by ForEachExprWhere.visit
• Full Lean CI is the authoritative validation

AI assistance

AI tools assisted with issue triage, duplicate-PR search, implementation inspection, and wording. I reviewed the traversal, deduplication state, and final one-file 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 f1053b60be68ce3149109206989f04eedb5d2239 --onto 5b8d06c1764fa367a1e27b3e89f64667eac425af. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-02 02:21:55)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 945e78b86645b179655123cd2fdba83d89d28d07 --onto 110db9cb751afaee8b2ac344887d6c7e632f77b4. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-04 02:16:21)

[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 f1053b60be68ce3149109206989f04eedb5d2239 --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-02 02:21:57)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 945e78b86645b179655123cd2fdba83d89d28d07 --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-04 02:16:22)

[nomeata]

I see you updated these branches. Did you see my message on the Lean Zulip?