perf: do not consult isNoConfusion in whnf

[nomeata]

This PR lets whnf not consult isNoConfusion, to speed up this hot path a bit.

[nomeata]

!radar

[leanprover-radar]

Benchmark results for 11a3329 against 1d0d391 are in! @nomeata

Major changes (2)

• ✅ build//instructions: -50.2G (-0.4%)
• ✅ bv_decide_rewriter.lean//instructions: -350.2M (-1.8%)

Minor changes (5)

• ✅ Init.Data.BitVec.Lemmas re-elab//instructions: -6.2G (-0.7%)
• ✅ Init.Data.BitVec.Lemmas//instructions: -1.2G (-0.8%)
• ✅ grind_bitvec2.lean//instructions: -1.7G (-0.8%)
• ✅ grind_list2.lean//instructions: -403.6M (-0.6%)
• ✅ riscv-ast.lean//instructions: -730.6M (-0.5%)

[leanprover-bot]

Reference manual CI status:

• ✅ Reference manual branch lean-pr-testing-11571 has successfully built against this PR. (2025-12-09 23:37:16) View Log
• 🟡 Reference manual branch lean-pr-testing-11571 build against this PR didn't complete normally. (2025-12-09 23:37:28) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-11571 has successfully built against this PR. (2025-12-10 00:30:52) View Log

[Kha]

!bench mathlib

(my first try using it)

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@2ee6d2d against leanprover-community/mathlib4-nightly-testing@bbf1f53 are in! @Kha

Minor changes (2)

• ✅ build/module/Mathlib.RingTheory.DedekindDomain.Different//instructions: -6.2G (-1.6%)
• ✅ build/module/Mathlib.RingTheory.Polynomial.UniversalFactorizationRing//instructions: -6.3G (-1.7%)