mathlib

4da83134 - feat(category_theory/closed): golf definition and proofs (#5623)

feat(category_theory/closed): golf definition and proofs (#5623) Using the new mates framework, simplify the definition of `pre` and shorten proofs about it. To be more specific, - `pre` is now explicitly a natural transformation, rather than indexed morphisms with a naturality property - The new definition of `pre` means things like `pre_map` which I complained about before are easier to prove, and `pre_post_comm` is automatic - There are now more lemmas relating `pre` to `coev`, `ev` and `uncurry`: `uncurry_pre` in particular was a hole in the API. - `internal_hom` has a shorter construction. In particular I changed the type to `Cᵒᵖ ⥤ C ⥤ C`, which I think is better since the usual external hom functor is given as `Cᵒᵖ ⥤ C ⥤ Type*`, so this is consistent with that. In a subsequent PR I'll do the same for `exp_comparison`, but that's a bigger change with improved API so they're separate for now.