mathlib3

e902cae5 - feat(category_theory/limits/cofinal): better API for cofinal functors (#4276)

feat(category_theory/limits/cofinal): better API for cofinal functors (#4276) This PR 1. Proves that `F : C ⥤ D` being cofinal is equivalent to `colimit (F ⋙ G) ≅ colimit G` for all `G : D ⥤ E`. (Previously we just had the implication.) 2. Proves that if `F` is cofinal then `limit (F.op ⋙ H) ≅ limit H` for all `H: Dᵒᵖ ⥤ E`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>