Commit 2020-10-30 05:28 4003b3ee

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