mathlib3

857cbd52 - chore(category_theory/limits/preserves): split up files and remove redundant defs (#4717)

chore(category_theory/limits/preserves): split up files and remove redundant defs (#4717) Broken off from #4163 and #4716. While the diff of this PR is quite big, it actually doesn't do very much: - I removed the definitions of `preserves_(co)limits_iso` from `preserves/basic`, since there's already a version in `preserves/shapes` which has lemmas about it. (I didn't keep them in `preserves/basic` since that file is already getting quite big, so I chose to instead put them into the smaller file. - I split up `preserves/shapes` into two files: `preserves/limits` and `preserves/shapes`. From my other PRs my plan is for `shapes` to contain isomorphisms and constructions for special shapes, eg `fan.mk` and `fork`s, some of which aren't already present, and `limits` to have things for the general case. In this PR I don't change the situation for special shapes (other than simplifying some proofs), other than moving it into a separate file for clarity.