This is the long overdue instance has_mem (set α) (filter α). It gets rid of countless .sets and parentheses, and make every filter use closer to the real world thing. There are still a couple of inconveniences: of course we still have a couple of lemmas about the sets of a filter, and rewriting using them is not always possible, even though the instance is reducible. The workaround is to add a couple of show or change, or type ascriptions when using the funny triangle. I also added mem_infi to replace many uses of infi_sets_eq.

A weirder thing is in asymptotics.lean where use times out. I replaced those bby refine and everything works smoothly.