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/Adjunction/Over.lean

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

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