feat(category_theory/adjunction): complete well-powered category with a coseparating set is cocomplete

[TwoFX]

This corollary of the special adjoint functor theorem immediately implies that Grothendieck categories are complete, which, according to the Wikipedia article on Grothendieck categories, is "a rather deep result".

---

• [x] depends on: #15796
• [ ] depends on: #15859
• [ ] depends on: #15912
• [ ] depends on: #15981
• [ ] depends on: #15987

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#15796~~
• ~~leanprover-community/mathlib#15859~~
• ~~leanprover-community/mathlib#15912~~
• ~~leanprover-community/mathlib#15981~~
• ~~leanprover-community/mathlib#15987~~ By Dependent Issues (🤖). Happy coding!

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests