mathlib3

cea97d9a - feat(*): add not_mem_of_not_mem_closure for anything with subset_closure (#9595)

feat(*): add not_mem_of_not_mem_closure for anything with subset_closure (#9595) This is a goal I would expect library search to finish if I have something not in a closure and I want it not in the base set.