feat: define `pp_using_anonymous_constructor` attribute and apply it

[kmill]

Implements a Lean 3 pretty printer feature. Structures with the @[pp_using_anonymous_constructor_attribute] pretty print like ⟨x, y, z⟩ rather than {a := x, b := y, c := z}.

Adds this attribute to the following core types: Sigma, PSigma, PProd, Subtype, And, and Fin. These types had this attribute in Lean 3.

Zulip discussion

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std CI can not be attempted yet, as the nightly-testing-2024-03-09 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-03-09 17:55:02)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 085d01942d5bfea2461b9fab95438a4c2ed1b56d --onto 2c15cdda044e77bb8c3937c63501850790e60dc6. (2024-03-21 23:03:05)

[nomeata]

Thanks a lot! Pretty please enable this for PProd, it'll make my life dealing with well-founded recursion so much better :-)

[kmill]

@nomeata It's already been done in #3735 😃 (this needed a stage0 update first)