chore(category/limits/opposites): instances (#16511)
Upgrade some lemmas to instances, per [zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/limits.20in.20opposite.20categories).
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
