∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (W : CategoryTheory.MorphismProperty C) (D : Type u_4)
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D] (x : CategoryTheory.Functor W.Localization D),
  W.IsInvertedBy (W.Q.comp x)