Commit 2023-07-03 14:48 ceaa4ecb

View on Github →

refactor: move all register_simp_attrs to 1 file (#5681) There are slight differences between mathlib3 and mathlib4 (different set of attributes, different lemmas are in core/std), so I redid the same refactor instead of forward-porting changes. mathlib3 PR: leanprover-community/mathlib#19223

Estimated changes

modified theorem Functor.map_id
modified theorem Set.mem_setOf_eq
modified theorem Function.comp.left_id
modified theorem Function.comp.right_id
modified theorem Equiv.invFun_as_coe
modified def Equiv.sigmaEquivProd
modified theorem Equiv.toFun_as_coe