Commit 2026-01-16 16:52 6969ea8d

View on Github →

feat: push for Set membership (#34023) This PR adds @[push] tags for set membership. This is a subset of #30042, namely all the Set tags. #30042 also has tags for Finset and Multiset; as Set is the biggest use case of these, we start with just these.

Estimated changes

modified theorem Set.mem_diagonal_iff
modified theorem Set.mem_pi
modified theorem Set.mem_range
modified theorem Set.mem_Icc
modified theorem Set.mem_Ico
modified theorem Set.mem_Iic
modified theorem Set.mem_Iio
modified theorem Set.mem_Ioc
modified theorem Set.mem_Ioo