Better treatment of auto parameters when filling placeholders

[SReichelt]

Currently, when filling placeholders related to structures such as groups, the selection of possible terms does not behave optimally:

• Since the defining characteristic of such structures is that they are based on an arbitrary set, there are often no type restrictions on a given placeholder, i.e. all possible terms type-check. However, only very few of these terms actually lead to a useful result; the majority are not related in any way to the structure in question. In particular, most terms lead to a result where the auto parameter specifying the structure cannot be inferred automatically. It would be nice to filter out such useless choices, but care must be taken not to filter out too much. E.g. it should always remain possible to select generic things like "function value", which can in fact lead to an auto-fillable result depending on the function used.
• On the other hand, for concrete structures (symmetric group, ring of integers, ...), there should actually be a way to infer the structure, similarly to how type classes work in Lean (and canonical structures in Coq?). As a concrete example, if the binomial theorem is invoked with three variables that are natural numbers, the semiring argument should be inferred automatically as the semiring of natural numbers. More generally, each construction should refer to a list of concrete structures that apply to that construction (taking Add special support for forgetful functors #58 into account). This feature directly extends to concrete categories.

These two points are related in that the first crucially depends on the second; otherwise certain expressions can no longer be built using the GUI.

Might depend on #43. Also somewhat related to #61, as that issue also deals with more restrictive type checking of placeholders.