∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C},
  autoParam
      (∀ (J : Type w') [inst_1 : CategoryTheory.Category.{w, w'} J] [CategoryTheory.IsFiltered J],
        W.IsStableUnderColimitsOfShape J)
      CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits.isStableUnderColimitsOfShape._autoParam →
    CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits.{w, w', v, u} W