Commit 2025-06-12 11:49 cd1ed4f3

View on Github →

chore(Data/Set): move very basic lemmas earlier (#25707) Move basic projection lemmas about mem and setOf earlier so that you don't have to import order theory to use them (or for simp to see them)!

Estimated changes

deleted theorem Membership.mem.out
deleted theorem Set.eq_mem_setOf
deleted theorem Set.mem_setOf
deleted theorem Set.notMem_setOf_iff
deleted theorem Set.setOf_mem_eq