Commit 2026-01-11 14:20 83e7fe4c

feat(CategoryTheory): use push attribute for CategoryTheory.inv. (#33820) In this PR a few lemmas about isomorphisms are tagged @[push] or @[push ←]. The directionality of lemmas should be that the inv constant is pushed away from the head of the expression. Some annotations are terminal, for instance, the ones for inv (inv f) = f, or inv (e.hom) = e.inv and inv (e.inv) = e.hom. Running push inv thus normalizes inverses of expressions, though the form obtained is not necessarily the same as the simp normal form (simp normal forms in the library tend to "pull" the inverses outwards, while the push lemmas here are pushing them inwards). These annotations will serve as building blocks for a simproc that cancels an isomorphism with its inverse within arbitrary nested expressions (functor compositions, whiskering in monoidal categories, natural isomorphisms of multifunctors, etc.). See #33822 for the implementation of the simproc, and how it uses the annotations introduced here.