Commit 2021-10-31 17:26 f2b77d7d

refactor(set_theory/cardinal): swap sides of simp lemmas (#10040)

API changes

Swap sides of simp lemmas

• cardinal.add_def is no loner a simp lemma, cardinal.mk_sum (renamed from cardinal.add) simplifies #(α ⊕ β) to lift.{v u} (#α) + lift.{u v} (#β);
• cardinal.mul_def is no loner a simp lemma, cardinal.mk_prod (merged with cardinal.mul) simplifies #(α × β) to lift.{v u} (#α) * lift.{u v} (#β);
• cardinal.power_def is no longer a simp lemma. New lemma cardinal.mk_arrow computes #(α → β). It is not a simp lemma because it follows from other simp lemmas.
• replace cardinal.sum_mk with cardinal.mk_sigma and cardinal.prod_mk with cardinal.mk_pi;

Other changes

• new lemmas @[simp] cardinal.lift_uzero and cardinal.lift_umax';
• split cardinal.linear_order into cardinal.preorder (doesn't rely on classical.choice), cardinal.partial_order (needs classical.choice, computable), and cardinal.linear_order (noncomputable);
• add cardinal.lift_order_embedding;
• add cardinal.mk_psum;
• rename cardinal.prop_eq_two to cardinal.mk_Prop, drop the old mk_Prop;
• use local notation for natural power;
• rename old sum_const to sum_const', the new @[simp] lemma sum_const is what used to be sum_const_eq_lift_mul;
• rename old prod_const to prod_const', the new @[simp] lemma prod_const deals with types in different universes;
• add @[simp] to cardinal.prod_eq_zero and cardinal.omega_le_mk;
• add @[simp] lemmas cardinal.mk_eq_one, cardinal.mk_vector, cardinal.omega_mul_eq, and cardinal.mul_omega_eq;
• replace mk_plift_of_true and mk_plift_of_false with mk_plift_true and mk_plift_false;
• mk_list_eq_mk and mk_finset_eq_mk now assume [infinite α] instead of ω ≤ #α.