chore: adaptations for nightly-2024-06-12

[kim-em]

This includes adaptations for:

• feat: dsimprocs for ite and dite leanprover/lean4#4430
• perf: a isDefEq friendly Fin.sub leanprover/lean4#4421
• chore: unify String.csize : Nat and Char.utf8Size : UInt32 as Char.size : Nat leanprover/lean4#4357
• fix: rw should not include existing goal metavariables in the resulting subgoals leanprover/lean4#4385
• fix: universe parameter order discrepancy between theorem and def leanprover/lean4#4408

Sorry that it's a few days worth in one go, for various reasons it was hard to get to green during this period.

[github-actions]

PR summary a6a547cd51

Import changes

No significant changes to the import graph

---

Declarations diff

+ neg_def
-+-+ norm_eq_ciSup

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[jcommelin]

bors d+

[mathlib-bors]

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.