Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-28 15:21 40da087f

View on Github →

feat(equiv/basic): use @[simps] (#4652) Use the @[simps] attribute to automatically generate equation lemmas for equivalences. The names foo_apply and foo_symm_apply are used for the projection lemmas of foo.

Estimated changes

modified def equiv.Pi_congr_left'
deleted theorem equiv.arrow_congr'_apply
modified def equiv.arrow_congr
deleted theorem equiv.arrow_congr_apply
deleted theorem equiv.coe_of_bijective
deleted theorem equiv.coe_plift
deleted theorem equiv.coe_plift_symm
deleted theorem equiv.coe_prod_comm
deleted theorem equiv.coe_prod_congr
deleted theorem equiv.coe_ulift
deleted theorem equiv.coe_ulift_symm
deleted theorem equiv.conj_apply
modified def equiv.fun_unique
deleted theorem equiv.fun_unique_apply
deleted theorem equiv.of_injective_apply
modified def equiv.prod_assoc
deleted theorem equiv.prod_assoc_apply
modified def equiv.prod_comm
modified def equiv.prod_congr
modified def equiv.prod_punit
deleted theorem equiv.prod_punit_apply
deleted theorem equiv.punit_prod_apply
deleted theorem equiv.set.image_apply
deleted theorem equiv.set.of_eq_apply
deleted theorem equiv.set.range_apply
deleted theorem equiv.set.univ_apply
deleted theorem equiv.set.univ_symm_apply
deleted theorem equiv.sum_comm_apply
deleted theorem equiv.sum_congr_apply
modified def subtype.coind
modified def subtype.map