refactor(library/data/unit): break unit.lean into smaller pieces

The unit datatype is used by automation.

We want to be able to access its declaration without having to access
all dependencies (e.g., decidable, subsingleton, inhabited, ...).

This is *not* an optimization, but a way to make sure we can "import" unit
before we import other declarations.
fix(library/definitional): make sure argument is an inductive datatype
chore(library/definitional): remove dead code
feat(library/definitional/cases_on): automatically add 'cases_on'
fix(frontends/lean/inductive_cmd): include 'induction_on', 'cases_on', and 'rec_on' into .ilean index file
fix(library/data/unit): missing file
fix(emacs/lean-syntax): syntax highlight for composite names in declarations
fix(frontends/lean/parser): add two kinds of no_undef_id behavior: to (global) constant; to local constant
fix(frontends/lean/parser): save identifier info for undef local
feat(library/tactic/exact_tactic): modify 'exact' tactic semantics, use higher-order unification

See new node.inj4 theorem, we need the extra power to be able to avoid type information at
    exact (assume e₁ e₂, e₁)
feat(emacs/lean-syntax): add 'eassumption' highlight
fix(frontends/lean): improve begin-end construct
fix(frontends/lean/elaborator): missing information when displaying unsolved placeholders
fix(frontends/lean/elaborator): nested begin-end bug
fix(frontends/lean/builtin_cmds): bug (name clashing) in 'check' command new meta-variable naming
test(tests/lean/run/sigma_no_confusion): define 'no_confusion' for sigma types
merged commit
foo
foo
cleaned up slice