PR !4#30042: feat(push): `@[push]` attributes for `∈` in ...

Stream: triage

[Random Issue Bot]

Today I chose PR #30042 for discussion!

feat(push): @[push] attributes for ∈ in Set, Finset and Multiset
Created by @Jovan Gerbscheid (@JovanGerb) on 2025-09-28
Labels: awaiting-author, merge-conflict, t-meta

Is this PR still relevant? Any recent updates? Anyone making progress?

[Jovan Gerbscheid]

This PR was a bit large. In the meantime, a smaller version of this PR, only for Set has been merged. If there is interest, I can make one for Finset next.

[Ruben Van de Velde]

If we have this for Set, then yes, I think it's important to have it for Finset too