mathlib3

feat(category_theory/equivalence): make definition of adjointify_η easier to elaborate

#1045

Merged