… are flat (leanprover#7302)

This PR changes how fields are elaborated in the `structure`/`class`
commands and also makes default values respect the structure resolution
order when there is diamond inheritance. Before, the details of
subobjects were exposed during elaboration, and in the local context any
fields that came from a subobject were defined to be projections of the
subobject field. Now, every field is represented as a local variable.
All parents (not just subobject parents) are now represented in the
local context, and they are now local variables defined to be parent
constructors applied to field variables (inverting the previous
relationship). Other notes:
- The entire collection of parents is processed, and all parent
projection names are checked for consistency. Every parent appears in
the local context now.
- For classes, every parent now contributes an instance, not just the
parents represented as subobjects.
- Default values are now processed according to the parent resolution
order. Default value definition/override auxiliary definitions are
stored at `StructName.fieldName._default`, and inherited values are
stored at `StructName.fieldName._inherited_default`. Metaprograms no
longer need to look at parents when doing calculations on default
values.
- Default value omission for structure instance notation pretty printing
has been updated in consideration of this.
- Now the elaborator generates a `_flat_ctor` constructor that will be
used for structure instance elaboration. All types in this constructor
are put in "field normal form" (projections of parent constructors are
reduced, and parent constructors are eta reduced), and all fields with
autoParams are annotated as such. This is not meant for users, but it
may be useful for metaprogramming.
- While elaborating fields, any metavariables whose type is one of the
parents is assigned to that parent. The hypothesis is that, for the
purpose of elaborating structure fields, parents are fixed: there is
only *one* instance of any given parent under consideration. See the
`Magma` test for an example of this being necessary. The hypothesis may
not be true when there are recursive structures, since different values
of the structure might not agree on parent fields.

Other notes:
- The elaborator has been refactored, and it now uses a monad to keep
track of the elaboration state.
- This PR was motivation for leanprover#7100, since we need to be able to make all
parents have consistent projection names when there is diamond
inheritance.

Still to do:
- Handle autoParams like we do default values. Inheritance for these is
not correct when there is diamond inheritance.
- Avoid splitting apart parents if the overlap is only on proof fields.
- Non-subobject parent projections do not have parameter binder kinds
that are consistent with other projections (i.e., all implicit by
default, no inst implicits). This needs to wait on adjustments to the
synthOrder algorithm.
- We could elide parents with no fields, letting their projections be
constant functions. This causes some trouble for defeq checking however
(maybe leanprover#2258 would address this).

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](leanprover-community/mathlib4#12129 (comment))
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 `let`s 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 #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 #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](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Where.20is.20sSup.20defined.20on.20submodules.3F/near/499578795))
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.

* fix

* fix again

* chore: bump to nightly-2025-03-15

* fix

* harden script

* chore: bump to nightly-2025-03-16

* Update lean-toolchain for testing leanprover/lean4#7516

* lake update

* fixes for leanprover/lean4#7516

* fixes for leanprover/lean4#7516

* partial test fixes

* fix stacks

* "fix" eqns test

* Remove neg instance, there is one upstream now

* chore: bump to nightly-2025-03-17

* lake update

* lake update

* lint

* Update lean-toolchain for testing leanprover/lean4#7522

* Update lean-toolchain for testing leanprover/lean4#5182

* Bump batteries for leanprover/lean4#5182

* simp works

* Fewer unseal

* Trigger CI for leanprover/lean4#5182

* max heartbeats

* update test

* Update lean-toolchain for testing leanprover/lean4#7519

* Update lean-toolchain for testing leanprover/lean4#7302

* Fix

* fixes

* Trigger CI for leanprover/lean4#5182

* chore: bump to nightly-2025-03-18

* Less rfl abuse

* fix `compile_inductive%` regression

* Trigger CI for leanprover/lean4#5182

* Trigger CI for leanprover/lean4#5182

* Trigger CI for leanprover/lean4#5182

* Adapt

* process deprecations

* Update lean-toolchain for testing leanprover/lean4#7558

* Adapt

* deprecations

* chore: bump to nightly-2025-03-19

* chore: fixes for leanprover/lean4#7519

* Update lean-toolchain for testing leanprover/lean4#7544

* lake update

* fixes for leanprover/lean4#7544

* fixes for leanprover/lean4#7544

* fixes for leanprover/lean4#7544

* fixes for leanprover/lean4#7544

* Trigger CI for leanprover/lean4#7544

* .

* cleaning up

* chore: bump to nightly-2025-03-20

* update

* deprecation/note about upstreamed version

* fix

* Update lean-toolchain for testing leanprover/lean4#7614

* chore: bump to nightly-2025-03-21

* Adapt back

* fix test output

* chore: bump to nightly-2025-03-22

* Merge master into nightly-testing

* chore: adaptations for nightly-2025-03-22

* fix

* Merge master into nightly-testing

* protected

* chore: bump to nightly-2025-03-24

* update batteries and aesop

* fixes for count_cons_of_ne

* fix fix to Sym.inhabitedSym' (need `default`, not the `a` that happens to be in context)

* bump heartbeats in MathlibTest/observe

* fix, deprecated

* fix merge

* Update lean-toolchain for testing leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* update batteries

* fixes for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* update batteries

* fixes

* chore: bump to nightly-2025-03-25

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* update batteries

* Trigger CI for leanprover/lean4#7672

* one fix

* fixes

* maxheartbeats

* fixes for leanprover/lean4#7672

* fixes for leanprover/lean4#7672

* fixes for leanprover/lean4#7672

* fixes for leanprover/lean4#7672

* cleanups

* .

* chore: bump to nightly-2025-03-26

* update aesop

* Update lean-toolchain for testing leanprover/lean4#7690

* Trigger CI for leanprover/lean4#7690

* Trigger CI for leanprover/lean4#7690

* maxHeartbeats

* max heartbeats

* invalidate cache

* another heartbeats

* bump batteries

* deprecation

* Update lean-toolchain for testing leanprover/lean4#7692

* Delete

* chore: bump to nightly-2025-03-27

* update batteries

* bump batteries

* many more maxHeartbeats

* chore: bump leantar v0.1.15

* invalidate cache

* cache flush, take 2

* feat(Cache): root hash generation counter

* 1-line fix

* chore: bump to nightly-2025-03-28

* update deps

* remove upstreamed

* remove all adaptation notes, hooray

* merge lean-pr-testing-7692

* fixes from Kevin's review

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>