Commit 2021-06-17 17:10 97843966

View on Github →

refactor(order/preorder_hom): golf and simp lemmas (#7429) The main change here is to adjust simps to generate coercion lemmas rather than .to_fun for preorder_hom, which allows us to auto-generate some simp lemmas.

Estimated changes

Modified src/algebraic_topology/simplex_category.lean

Modified src/order/category/Preorder.lean

Modified src/order/omega_complete_partial_order.lean

modified def omega_complete_partial_order.chain.map

Modified src/order/preorder_hom.lean

deleted theorem order_embedding.to_preorder_hom_coe

modified theorem preorder_hom.coe_fun_mk

deleted theorem preorder_hom.coe_id

deleted theorem preorder_hom.coe_inj

modified theorem preorder_hom.ext

added theorem preorder_hom.to_fun_eq_coe

deleted theorem rel_hom.to_preorder_hom_coe_fn

Modified src/topology/omega_complete_partial_order.lean