Commit 2025-06-02 01:02 1414404d

feat(Tactic/CategoryTheory): extension of reassoc to equality of isomorphisms (#24303) Extend the reassoc attribute so that it can also generate _assoc variants of lemmas of shape ∀ .., f = g, where f g : X ≅ Y. We similarly extend reassoc_of%. We also provide a very basic test suite for this extension.