Commit 2020-05-18 13:38 2fa1d7cd

View on Github →

Revert "fix(category_theory/eq_to_hom): remove bad simp lemmas (#1346)" (#2713) These are good simp lemmas: they push things into a proof-irrelevant position. This reverts commit 5a309a3aa30fcec122a26f379f05b466ee46fc7a.

Estimated changes

Modified src/category_theory/eq_to_hom.lean

modified theorem category_theory.eq_to_hom_app

modified theorem category_theory.eq_to_hom_map

modified theorem category_theory.eq_to_iso_map