mathlib

b0473968 - feat(data/set/finite): add a version of `prod_preimage` for `inj_on` (#3342)

feat(data/set/finite): add a version of `prod_preimage` for `inj_on` (#3342) * rename `finset.prod_preimage` to `finset.prod_preimage_of_bij`; * new `prod_preimage` assumes `∀ x ∈ s, x ∉ range f, g x = 1`; * rename `finset.image_preimage` to `finset.image_preimage_of_bij`; * new `finset.image_preimage` says `image f (preimage s hf) = s.filter (λ x, x ∈ set.range f)`; * change the order of implicit arguments in the definition of `set.inj_on`; * add `prod_filter_of_ne`; * use `coe` instead of `subtype.val` in `prod_attach`; * add `finset.image_subset_iff`, `finset.image_subset_iff_subset_preimage`, `finset.map_subset_iff_subset_preimage`.