Commit 2020-10-28 07:49 6dfa952c

refactor(order/filter): make filter.has_mem semireducible ([#4807](https://github.com/leanprover-community/mathlib/pull/4807)) This way simp only []does not simplifys ∈ ftos ∈ f.sets`.

• Add protected simp lemmas filter.mem_mk and filter.mem_sets.
• Use implicit argument in filter.mem_generate_iff.
• Use ∃ t, s ∈ ... instead of s ∈ ⋃ t, ... in filter.mem_infi_finite and filter.mem_infi_finite'.
• Use an implicit argument in (non/ne_)empty_of_mem_ultrafilter.