fix: reduce binder types in reduceAll

[sankalpsthakur]

This PR makes reduce visit lambda and forall binder types when type reduction is enabled.

The previous lambda/forall cases opened the original binders and reduced only the body. Consequently, reduceAll could return an expression such as Foo → True even when Foo reduces to True.

Reuse the existing binder traversal helpers, which visit each domain and the body in the correct local context. The existing skipTypes guard preserves the default behavior of reduce.

Closes #6084

Validation

• Added tests/elab/issue6084.lean
• Exact PR-history search found no competing implementation
• Full Lean CI is the authoritative validation

AI assistance

AI tools assisted with issue triage, source inspection, implementation, and regression preparation. I reviewed the binder traversal helpers and final five-line production 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 23d17351ab630c393aadb7f8c97ef9b8ee633cdb --onto 5b8d06c1764fa367a1e27b3e89f64667eac425af. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-02 06:58: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:13:10)

[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 23d17351ab630c393aadb7f8c97ef9b8ee633cdb --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-02 06:58: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:13:12)