feat(category_theory/limits/preserves): transfer preserving limits through nat iso (#4932)
- Move two defs higher in the file
- Shorten some proofs using newer lemmas
- Show that we can transfer preservation of limits through natural isomorphism in the functor.