mathlib3

dcd5ebd9 - feat({data/{finset,set},order/filter}/pointwise): More lemmas (#14216)

feat({data/{finset,set},order/filter}/pointwise): More lemmas (#14216) Lemmas about `s ^ n`, `0 * s` and `1 ∈ s / t`. Other changes: * `finset.mul_card_le` → `finset.card_mul_le` * `finset.card_image_eq_iff_inj_on` → `finset.card_image_iff`. * `zero_smul_subset` → `zero_smul_set_subset` * Reorder lemmas slightly * Add an explicit argument to `finset.coe_smul_finset` * Remove an explicit argument to `set.empty`