fix(frontends/lean): process choice-exprs at check_constant_next
refactor(library/data): rename prod_ext and dpair_ext to prod.eta and sigma.eta

Reason: they will be generated automatically by definitional package.
feat(frontends/lean/structure_cmd): add structure_cmd core
test(tests/lean/run): add structure command test
fix(frontends/lean/structure_cmd): 'rec' must be marked as protected
fix(frontends/lean): alias generation for composite names was not working

This is an issue for declarations that generate composite names such as
the inductive datatype packacke.

The commit also fix a bug in the generate of aliases for recursors
feat(frontends/lean/structure_cmd): add aliases for structure decls
fix(frontends/lean/decl_cmds): do not save 'examples' in .ilean file
feat(frontends/lean/structure_cmd): add coercions to parent structures
feat(frontends/lean/structure_cmd): mark structure as 'class' when [class] modifier is used
feat(frontends/lean/structure_cmd): mark coercion to parents as coercions and instances (when both structures as classes)
fix(emacs/lean-syntax): bug in syntax highlight, examples do not have names
feat(frontends/lean/structure_cmd): add 'eta' theorem for structures
fix(library/definitional): add missing files
refactor(library): major changes in the library

I made some major changes in the library. I wanted to wait with pushing
until I had finished the formalization of the slice functor, but for
some reason that is very hard to formalize, requiring a lot of casts and
manipulation of casts. So I've not finished that yet.

Changes:

- in multiple files make more use of variables

- move dependent congr_arg theorems to logic.cast and proof them using heq (which doesn't involve nested inductions and fewer casts).

- prove some more theorems involving heq, e.g. hcongr_arg3 (which do not
  require piext)

- in theorems where casts are used in the statement use eq.rec_on
  instead of eq.drec_on

- in category split basic into basic, functor and natural_transformation

- change the definition of functor to use fully bundled
categories. @avigad: this means that the file semisimplicial.lean will
also need changes (but I'm quite sure nothing major).  You want to
define the fully bundled category Delta, and use only fully bundled
categories (type and ᵒᵖ are notations for the fully bundled
Type_category and Opposite if you open namespace category.ops). If you
want I can make the changes.

- lots of minor changes
fix(tests/lean): to reflect changes in the standard library
refactor(library): use new 'structure' command to define prod and sigma
fix(frontends/lean/structure_cmd): modify coercion generation

The previous coercion was more efficient, but the computation was
getting stuck when processing algebraic structures
feat(frontends/lean/structure_cmd): allow structure declarations that contains only a header
feat(frontends/lean/structure_cmd): use 'mk' as constructor name when it is not provided