mathlib

6dfa952c - refactor(order/filter): make `filter.has_mem semireducible (#4807)

refactor(order/filter): make `filter.has_mem semireducible (#4807) This way `simp only []` does not simplify `s ∈ f` to `s ∈ 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`.