[#14501] chore: prefer dite over dif in identifiers

[downstream-lean4]

This is the adaptation PR for leanprover/lean4#14501.

[downstream-lean4]

Build report for downstream: undo overrides

Recently turned red:

Repo	Critical	Build	Test	Lint
aesop	✅	⏭️	⏭️	⏭️
batteries	✅	🟥 in 0m	⏭️	⏭️
mathlib4	✅	⏭️	⏭️	⏭️
reference-manual	✅	🟥 in 0m	⏭️	⏭️
cslib		⏭️	⏭️	⏭️

Unchanged

Repo	Critical	Build	Test	Lint
import-graph	✅	✅ in 0m	✅ in 0m	⏭️
lean4-cli	✅	✅ in 0m	✅ in 0m	⏭️
plausible	✅	✅ in 0m	✅ in 0m	⏭️
ProofWidgets4	✅	✅ in 0m	✅ in 0m	⏭️
quote4	✅	✅ in 0m	✅ in 0m	⏭️
BibtexQuery		✅ in 0m	⏭️	⏭️
comparator		✅ in 0m	⏭️	⏭️
doc-gen4		✅ in 0m	⏭️	⏭️
illuminate		✅ in 0m	✅ in 0m	⏭️
lean4-unicode-basic		✅ in 0m	✅ in 0m	⏭️
lean4export		✅ in 0m	✅ in 0m	⏭️
LeanSearchClient		✅ in 0m	✅ in 0m	⏭️
leansqlite		✅ in 0m	✅ in 0m	⏭️
repl		✅ in 0m	✅ in 0m	⏭️
verso		✅ in 1m	✅ in 1m	⏭️
verso-slides		🟥 in 0m	⏭️	⏭️
verso-web-components		✅ in 0m	⏭️	⏭️

View run

[downstream-lean4]

The automatic merge failed. @TwoFX, please fix any merge conflicts and merge this PR manually.

[TwoFX]

Superseded by leanprover-community/mathlib4-nightly-testing@b746661