chore: simplify bif to if

[TwoFX]

This PR turns cond_eq_ite into a simp lemma.

This means that users of cond now automatically benefit from the better lemma coverage of ite.

We also prefer if over bif in some definitions, establishing the pattern of using ite instead of cond unless there is a demonstrated benefit to using cond.

[downstream-lean4]

The adaptation PR for this PR is leanprover/downstream-lean4#20.

[TwoFX]

!radar

[leanprover-radar]

Benchmark results for 44e5d21 against 0bfc3ac are in. No significant results found. @TwoFX

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run build differ between commits.
• Bench repo commit hashes for run other differ between commits.

• ✅ build//instructions: -118.5M (-0.00%)

Medium changes (1🟥)

• 🟥 build/profile/grind dsimp//wall-clock: +3ms (+86.20%)

Small changes (1✅, 6🟥)

• 🟥 build/module/Init.Data.Bool//instructions: +24.9M (+0.57%)
• ✅ build/module/Init.Data.List.Erase//instructions: -34.1M (-0.48%)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide//instructions: +17.6M (+1.76%)
• 🟥 build/module/Std.Data.Internal.List.Associative//instructions: +301.4M (+0.38%)
• 🟥 build/module/Std.Tactic.BVDecide.Normalize.BitVec//instructions: +106.8M (+2.43%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Tactic.BVDecide.Normalize.Bool//instructions: +86.0M (+3.24%) (reduced significance based on absolute threshold)
• 🟥 misc/import Std.Data.Internal.List.Associative//instructions: +322.2M (+0.49%)

[leanprover-bot]

Reference manual CI status:

• ✅ Reference manual branch lean-pr-testing-14588 has successfully built against this PR. (2026-07-29 12:27:37) View Log
• 🟡 Reference manual branch lean-pr-testing-14588 build against this PR didn't complete normally. (2026-07-29 12:27:51) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-14588 build failed against this PR. (2026-07-29 12:28:08) View Log