Commit 2026-01-30 12:44 52e75dc9

feat(CategoryTheory/Iso): use to_dual for X ≅ Y (#34008) This PR uses to_dual for isomorphisms in category theory. There are two possible designs:

• to_dual could swap the arguments, turning X ≅ Y into Y ≅ X
• to_dual could leave the arguments in place, and instead translate Iso.hom to Iso.inv and vice versa I went with the second option, because I think it is more sensible. In a sense, X ≅ Y is to X ⟶ Y what a = b is to a ≤ b, and we also do not swap the arguments in a = b, even though it would be possible. Notes:
• The new ext_inv dual of ext is hard to generate automatically for to_dual for various reasons, so it is proved manually.
• When applying simps on a definition of type _ ≅ _, the generated _hom and _inv lemmas need to be manually tagged as dual to eachother with to_dual existing, with a set_option linter.existingAttributeWarning false in.
• I used to_dual none a few times to avoid adding too many redundant declarations to the API.
• I added no_expose to inv, with the reason that to_dual cannot translate proofs that unfold inv. And if the value isn't exported, then inv also cannot be unfolded. Nobody should rely on this anyways since it is just a Classical.choose. Two proofs had to be fixed as a result, which was easy to do with grind.
• I removed the outdated porting notes on asIso_hom and asIso_inv.