This PR changes how {...}/where notation ("structure instance notation") elaborates. The notation now tries to simulate a flat representation as much as possible, without exposing the details of subobjects. Features:

• When fields are elaborated, their expected types now have a couple reductions applied. For all projections and constructors associated to the structure and its parents, projections of constructors are reduced and constructors of projections are eta reduced, and also implementation detail local variables are zeta reduced in propositions (so tactic proofs should never see them anymore). Furthermore, field values are beta reduced automatically in successive field types. The example in mathlib4#12129 now shows a goal of 0 = 0 rather than { toFun := fun x => x }.toFun 0 = 0.
• All parents can now be used as field names, not just the subobject parents. These are like additional sources but with three constraints: every field of the value must be used, the fields must not overlap with other provided fields, and every field of the specified parent must be provided for. Similar to sources, the values are hoisted to lets if they are not already variables, to avoid multiple evaluation. They are implementation detail local variables, so they get unfolded for successive fields.
• All class parents are now used to fill in missing fields, not just the subobject parents. Closes Field missing on diamond-shaped instances #6046. Rules: (1) only those parents whose fields are a subset of the remaining fields are considered, (2) parents are considered only before any fields are elaborated, and (3) only those parents whose type can be computed are considered (this can happen if a parent depends on another parent, which is possible since feat: change structure command to elaborate fields as if structures are flat #7302).
• Default values and autoparams now respect the resolution order completely: each field has at most one default value definition that can provide for it. The algorithm that tries to unstick default values by walking up the subobject hierarchy has been removed. If there are applications of default value priorities, we might consider it in a future release.
• The resulting constructors are now fully packed. This is implemented by doing structure eta reduction of the elaborated expressions.
• "Magic field definitions" (as reported on Zulip) have been eliminated. This was where fields were being solved for by unification, tricking the default value system into thinking they had actually been provided. Now the default value system keeps track of which fields it has actually solved for, and which fields the user did not provide. Explicit structure fields (the default kind) without any explicit value definition will result in an error. If it was solved for by unification, the error message will include the inferred value, like "field 'f' must be explicitly provided, its synthesized value is v"
• When the notation is used in patterns, it now no longer inserts fields using class parents, and it no longer applies autoparams or default values. The motivation is that one expects patterns to match only the given fields. This is still imperfect, since fields might be solved for indirectly.
• Elaboration now attempts error recovery. Extraneous fields log errors and are ignored, missing fields are filled with sorry.

This is a breaking change, but generally the mitigation is to remove dsimp only from the beginnings of proofs. Sometimes "magic fields" need to be provided — four possible mitigations are (1) to provide the field, (2) to provide _ for the value of the field, (3) to add .. to the structure instance notation, (4) or decide to modify the structure command to make the field implicit. Lastly, sometimes parent instances don't apply when they should. This could be because some of the provided fields overlap with the class, or it could be that the parent depends on some of the fields for synthesis — and as parents are only considered before any fields are elaborated, such parents might not be possible to use — we will look into refining this further.

There is also a change to elaboration: now the afterTypeChecking attributes are run with all structure data set up (e.g. the list of parents, along with all parent projections in the environment). This is necessary since attributes like @[ext] use structure instance notation, and the notation needs all this data to be set up now.