Forgetful functor from Over X preserves cofiltered limits

Note that Over.forget X : Over X ⥤ C already preserves all colimits because it is a left adjoint. See Mathlib/CategoryTheory/Comma/Over/Pullback.lean

instance CategoryTheory.Limits.instPreservesCofilteredLimitsOfSizeOverForget {C : Type u_1} [Category.{v_1, u_1} C] {X : C} : PreservesCofilteredLimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1} (Over.forget X)

instance CategoryTheory.Limits.instPreservesFilteredColimitsOfSizeUnderForget {C : Type u_1} [Category.{v_1, u_1} C] {X : C} : PreservesFilteredColimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1} (Under.forget X)