Commit 2022-05-29 09:04 6b936a9d

View on Github →

feat(data/set/basic): simp-normal form for ↥{x | p x} (#14441) We make {x // p x} the simp-normal form for ↥{x | p x}. We also rewrite some lemmas to use the former instead of the latter.

Estimated changes

Modified archive/imo/imo1987_q1.lean

Modified src/algebra/algebraic_card.lean

modified theorem algebraic.cardinal_mk_le_max

modified theorem algebraic.cardinal_mk_le_mul

modified theorem algebraic.cardinal_mk_le_of_infinite

Modified src/data/set/basic.lean

added theorem set.coe_eq_subtype

added theorem set.coe_set_of

deleted theorem set.set_coe_eq_subtype

Modified src/set_theory/cardinal/basic.lean

added theorem cardinal.mk_subtype_le_omega

Modified src/set_theory/cardinal/cofinality.lean

Modified src/set_theory/cardinal/ordinal.lean

Modified src/tactic/subtype_instance.lean