feat(*): a, switch to lean 3.23 (#4802)
There are three changes affecting mathlib:
1. `ℕ → ℕ` is now elaborated as `∀ ᾰ : ℕ, ℕ`. This means that `intro` introduces assumptions with names like `ᾰ_1`, etc. These names should not be used, and instead provided explicitly to `intro` (and other tactics).
2. The heuristic to determine the definition name for `instance : foo bar` has been changed.
3. `by_contra` now uses classical logic, and defaults to the hypothesis name `h`.
4. adds a few new simp-lemmas in `data/typevec`
