feat(*): add lemmas, golf (#11294)
### New lemmas
* `function.mul_support_nonempty_iff` and `function.support_nonempty_iff`;
* `set.infinite_union`;
* `nat.exists_subseq_of_forall_mem_union` (to be used in an upcoming mass golfing of `is_pwo`/`is_wf`);
* `hahn_series.coeff_inj`, `hahn_series.coeff_injective`, `hahn_series.coeff_fun_eq_zero_iff`, `hahn_series.support_eq_empty_iff`;
* `nat.coe_order_embedding_of_set` (`simp` + `rfl`);
* `nat.subtype.of_nat_range`, `nat.subtype.coe_comp_of_nat_range`.
### Golfed proofs
* `set.countable.prod`;
* `nat.order_embedding_of_set_range`;
* `hahn-series.support_nonempty_iff`;
### Renamed
* `set.finite.union_iff` → `set.finite_union`, add `@[simp]` attr;
* `set.finite.diff` → `set.finite.of_diff`, drop 1 arg;
