Commit 2025-06-03 16:26 ea4aeae5

chore(CategoryTheory/Monoidal): define tensorLeft/Right as abbrev for curriedTensor (#24735) In the study of commutation of tensor products with colimits, we may not be completely sure about phrasing the assumptions (as instances) in terms of tensorLeft X (resp. tensorRight Y) or in terms of (curriedTensor C).obj X (resp. (curriedTensor C).flip.obj Y), even though they are defeq, and we could have to introduce lemmas/instances to deduce properties of tensorLeft X from that of (curriedTensor C).obj and vice versa. By making tensorLeft and tensorRight abbreviations, this PR makes such issues disappear.