mathlib3

cea27692 - chore(category_theory/adjunction/*): making arguments implicit in adjuction.comp and two small lemmas about mates (#15062)

chore(category_theory/adjunction/*): making arguments implicit in adjuction.comp and two small lemmas about mates (#15062) Working on adjunctions between monads and comonads, I noticed that adjunction.comp was defined with having the functors of one of the adjunctions explicit as well as the adjunction. However in the library, only `adjunction.comp _ _` ever appears. Thus I found it natural to make these two arguments implicit, so that composition of adjunctions can now be written as `adj1.comp adj2` instead of `adj1.comp _ _ adj2`. Furthermore, I provide two lemmas about mates of natural transformations to and from the identity functor. The application I have in mind is to the unit/counit of a monad/comonad in case of an adjunction of monads and comonads, as studied already by Eilenberg and Moore. Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>