enriched cotensors WIP PR to mathlib

Stream: Infinity-Cosmos

[Daniel Carranza]

I've created a PR to mathlib containing all code relating to defining the notion of enriched cotensors, proving the bifunctoriality, and proving that V itself has all cotensors.

https://github.com/leanprover-community/mathlib4/pull/35411

This PR is marked as WIP while I polish the file to adhere to the style guidelines. Pinging @Emily Riehl and @Arnoud van der Leer, who may have an interest in seeing the code.

There is one issue that seems beyond my understanding. The current version of this code introduces an abbrev definition Ehom V C x y for the hom-object C(x, y) in V. The intention is to make the code easier to read; the existing notation x \hom[V] y throws an error when instantiated at C = V (ambiguous term; Possible interpretations: (ihom x).obj y : V x ⟶[V] y : V). Moreover, there are a few calls to erw that stem from a failure to identify (ihom x).obj : V with Ehom V V x y. It seems there's some underlying issue that I'm not sure how to address?