Commit 2022-05-22 22:57 b7952ee5
View on Github →refactor(category_theory/shift): remove opaque_eq_to_iso (#14262)
It seems opaque_eq_to_iso was only needed because we had over-eager simp lemmas. After #14260, it is easy to remove.
refactor(category_theory/shift): remove opaque_eq_to_iso (#14262)
It seems opaque_eq_to_iso was only needed because we had over-eager simp lemmas. After #14260, it is easy to remove.