feat: parity between structure instance notation and where notation

[kmill]

This PR modifies structure instance notation and where notation to use the same notation for fields. Structure instance notation now admits binders, type ascriptions, and equations, and where notation admits full structure lvals. Examples of these for structure instance notation:

structure PosFun where
  f : Nat → Nat
  pos : ∀ n, 0 < f n

def p : PosFun :=
  { f n := n + 1
    pos := by simp }

def p' : PosFun :=
  { f | 0 => 1
      | n + 1 => n + 1
    pos := by rintro (_|_) <;> simp }

Just like for the structure where notation, a field f x y z : ty := val expands to f := fun x y z => (val : ty). The type ascription is optional.

The PR also is setting things up for future expansion. Pending some discussion, in the future structure/where notation could have have embedded where clauses; rather than { a := { x := 1, y := z } } one could write { a where x := 1; y := z }.

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-6165 build failed against this PR. (2024-11-21 23:21:57) View Log
• 💥 Mathlib branch lean-pr-testing-6165 build failed against this PR. (2024-11-22 01:58:49) View Log
• 💥 Mathlib branch lean-pr-testing-6165 build failed against this PR. (2024-11-30 03:06:34) View Log
• ✅ Mathlib branch lean-pr-testing-6165 has successfully built against this PR. (2024-11-30 04:03:44) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 734ea3071d67c3002867ccd767b8c3d80cc4e28d --onto 86f303774a7fbf38406ae13bd4b66f2753643a45. (2024-11-30 13:29:04)