[RFC] Create named goals for omitted fields in structure instances using `..` syntax

This entails modifying the structure instance elaborator such that .. in structure instances creates named goals for all omitted fields that cannot be synthesized via default values. This aids in interactive proofs that use refine. For example:

structure Foo where
  x : Nat
  y : Nat
  z : Nat := 0

example := by refine { x := 0, .. : Foo }; case y => exact 0

The goal ?y for the field y is created and named in the course of elaborating the structure instance, enabling one to write case y => .... (z assumes its default value 0.)

This modification only applies to structure instance syntax that is encountered outside of a pattern. Inside a pattern, the pre-existing behavior for .. is maintained, which simply fills all omitted fields with natural unnamed holes at the syntax level.

Note that existing uses of refine' that use { .. } are not broken.

I have code for this ready to go, and would be happy to make a PR if given the go-ahead! :)

Motivation

This functionality is currently needed for the ongoing port of mathlib. Several currently-ported files already expected this functionality to be available (as well as tactics which build on it) but needed to use workarounds, and more are soon to come.

In mathlib3 we used the refine_struct tactic to perform this task, but it’s less practical to use the same design in mathlib4. (For one, putting this in core instead of mathlib4 allows us to avoid excessive backtracking by the parser.)

Support for this functionality being implemented in core instead of mathlib has also been demonstrated on Zulip (albeit spread over a very long thread) and in mathlib porting meetings.

In addition to aiding the ongoing mathlib port, this provides an intrinsically useful aid for users writing interactive proofs. Structures are prevalent, and refining them—including interacting with and keeping track of the resulting goals—should be as easy and user-friendly as possible.

Start with the structure instance elaborator and compare .. handling outside patterns with its existing behavior inside patterns. Use the provided Foo example to verify that omitted non-default fields produce named goals while defaulted fields are synthesized, and confirm existing { .. } uses remain valid.