Commit 2024-07-31 09:13 f9821a61

chore: split conj into two files to streamline imports (#15300) This splits the file CategoryTheory.Conj into CategoryTheory.HomCongr and CategoryTheory.Conj. The point is that the latter requires much heavier imports than the former, while the former is all that is needed for CategoryTheory.Adjunction.Mates, which is used elsewhere. While making those changes, I added one theorem to the HomCongr file:

• A theorem map_isoCongr which parallels the existing map_homCongr. The proof is by ext; simp once the existing isoCongr is tagged with simps. In parallel, I've tagged the definition homCongr with simps and removed the theorem homCongr_apply which is automatically generated by simps.