mathlib

b7952ee5 - refactor(category_theory/shift): remove opaque_eq_to_iso (#14262)

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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>