Commit 2025-12-05 18:16 fe7877b4
View on Github →feat(Data/Finset/Empty): add @[push] tags for pushing negation (#32195)
This PR tags Finset.nonempty_iff_ne_empty and Finset.not_nonempty_iff_eq_empty with @[push], so that they can be used in push_neg, by_cases!, etc.
A bunch of proofs have been golfed using this.