mathlib3
2fa1d7cd - Revert "fix(category_theory/eq_to_hom): remove bad simp lemmas (#1346)" (#2713)

Commit
5 years ago
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.
Author
Parents
Loading