∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C)
  [inst_3 : L.IsLocalization W] (hF : W.IsInvertedBy F),
  (CategoryTheory.Localization.lift F hF L).IsRightDerivedFunctor (CategoryTheory.Localization.fac F hF L).inv W