mathlib

eae05105 - feat(category_theory/natural_isomorphism): a simp lemma cancelling inverses (#14299)

feat(category_theory/natural_isomorphism): a simp lemma cancelling inverses (#14299) I am not super happy to be adding lemmas like this, because it feels like better designed simp normal forms (or something else) could just avoid the need. However my efforts to think about this keep getting stuck on the shift functor hole we're in, and this lemma is useful in the meantime to dig my way out of it. :-) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>