Upstreaming `List.attach` and `Array.attach`

Stream: lean4

[llllvvuu]

I noticed this was mentioned positively here.

This would be very helpful since:

• termination checking failure on trees seems to be an FAQ (search "List.attach" in Zulip)
• sizeOf_list_dec is part of core, though it probably won't work without List.attach? (similarly for array_mem_dec)

The code footprint is small and the main thing to review would probably be

/--
Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
`List {x // P x}` is the same as the input `List α`.
(Someday, the compiler might do this optimization automatically, but until then...)
-/
@[inline] private unsafe def attachWithImpl
    (l : List α) (P : α → Prop) (_ : ∀ x ∈ l, P x) : List {x // P x} := unsafeCast l

which looks fine to me. May I advance this to an RFC?

[Mac Malone]

An RFC seems reasonable to me. :+1:

[llllvvuu]

https://github.com/leanprover/lean4/issues/4414