Commit 2026-07-31 08:20 0f0a217d

chore(CategoryTheory): remove backward options using implicit_reducible (#42161) This PR removes a lot of the transparency related set_option. I did this by using #defeq_abuse in to determine which definition was not being unfolded, and then tagging such definitions with implicit_reducible. In particular backward.isDefEq.respectTransparency can almost always be removed like this, but backward.defeqAttrib.useBackward is still sometimes tricky to remove. Presumably, the changes from this PR will let us remove many more set_option in further files that this PR doesn't touch.