chore(order/filter/basic): a few `simp` lemmas (#5685)
### Changes in `order/filter/basic`
* add `filter.inter_mem_sets_iff`;
* rename `filter.Inter_mem_sets` to `filter.bInter_mem_sets`, make it
an `iff` `[simp]` lemma;
* add a version `filter.bInter_finset_mem_sets` with a protected alias
`finset.Inter_mem_sets`;
* rename `filter.sInter_mem_sets_of_finite` to
`filter.sInter_mem_sets`, make it an `iff` `[simp]` lemma;
* rename `filter.Inter_mem_sets_of_fintype` to
`filter.Inter_mem_sets`, make it an `iff` `[simp]` lemma
* add `eventually` versions of the `*Inter_mem_sets` lemmas.
### New `@[mono]` attributes
* `set.union_subset_union` and `set.inter_subset_inter` instead of
`monotone_union` and `monotone_inter`; `mono*` failed to make a
progress with `s ∩ t ⊆ s' ∩ t'` goal.
* `set.image2_subset`
* `closure_mono`
