Commit 2022-01-07 12:43 6fb638b3

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;