mathlib

164c2e3c - chore(category_theory): attributes and a transport proof (#2751)

chore(category_theory): attributes and a transport proof (#2751) A couple of cleanups, modified a proof or two so that `@[simps]` can be used, which let me clean up some other proofs. Also a proof that we can transfer that `F` preserves the limit `K` along an isomorphism in `K`. (Preparation for some PRs from my topos project)