Commit 2024-12-13 19:15 5aaaf8b3

feat(CategoryTheory/Enriched): Add eHomCongr and related lemmas (#19932) Recall that when C is both a category and a V-enriched category, we say it is an EnrichedOrdinaryCategory if it comes equipped with an equivalence between morphisms X ⟶ Y in C and morphisms 𝟙_ V ⟶ (X ⟶[V] Y) in V that preserves identities and composition in C. In such a V-enriched ordinary category C, isomorphisms in C induce isomorphisms between hom-objects in V. We define this isomorphism, CategoryTheory.Iso.eHomCongr, and prove that it behaves nicely with respect to composition in C. The lemmas here parallel those for unenriched categories in Mathlib/CategoryTheory/HomCongr.lean and those for sorts in Mathlib/Logic/Equiv/Defs.lean (cf. Equiv.arrowCongr). Note, however, that they construct equivalences between Types and Sorts, respectively, while in this PR we construct isomorphisms between objects in V.