mathlib3

f3471479 - feat(category_theory): creation of limits and reflection of isomorphisms (#2426)

feat(category_theory): creation of limits and reflection of isomorphisms (#2426) Define creation of limits and reflection of isomorphisms. Part 2 of a sequence of PRs aiming to resolve my TODO [here](https://github.com/leanprover-community/mathlib/blob/cf89963e14cf535783cefba471247ae4470fa8c3/src/category_theory/limits/over.lean#L143) - that the forgetful functor from the over category creates connected limits. Remaining: - [x] Add an instance or def which gives that if `F` creates limits and `K ⋙ F` `has_limit` then `has_limit K` as well. - [x] Move the forget creates limits proof to limits/over, and remove the existing proof since this one is strictly stronger - make sure to keep the statement there though using the previous point. - [x] Add more docstrings Probably relevant to @semorrison and @TwoFX. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>