mathlib

183f4fce - refactor(category_theory/adjunction/mates): faster proof (#6116)

refactor(category_theory/adjunction/mates): faster proof (#6116) Co-authors: `lean-gptf`, Stanislas Polu elaboration 750ms -> 350ms 5X smaller proof term This was found by `formal-lean-wm-to-tt-m1-m2-v4-c4` when we evaluated it on theorems added to `mathlib` after we last extracted training data.