feat : port CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (#…

…3605)

This was harder than it looked (the proofs are long and broke).



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>

Mathlib.lean

@@ -506,6 +506,7 @@ import Mathlib.CategoryTheory.Limits.Creates
 import Mathlib.CategoryTheory.Limits.EssentiallySmall
 import Mathlib.CategoryTheory.Limits.ExactFunctor
 import Mathlib.CategoryTheory.Limits.Filtered
+import Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
 import Mathlib.CategoryTheory.Limits.Final
 import Mathlib.CategoryTheory.Limits.FullSubcategory
 import Mathlib.CategoryTheory.Limits.FunctorCategory