chore(data/fintype/card): review API (#4287)
API changes:
* `finset.filter_mem_eq_inter` now takes `[Π i, decidable (i ∈ t)]`; this way it works better
with `classical`;
* add `finset.mem_compl` and `finset.coe_compl`;
* [DRY] drop `finset.prod_range_eq_prod_fin` and `finset.sum_range_eq_sum_fin`:
use `fin.prod_univ_eq_prod_range` and `fin.sum_univ_eq_sum_range` instead;
* rename `finset.prod_equiv` to `equiv.prod_comp` to enable dot notation;
* add `fintype.prod_dite`: a specialized version of `finset.prod_dite`.
Also golf a proof in `analysis/normed_space/multilinear`
