∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E))
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (hF : W₁.IsInvertedBy₂ W₂ F)
  (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) [inst_5 : L₁.IsLocalization W₁]
  [inst_6 : L₂.IsLocalization W₂] [inst_7 : W₁.ContainsIdentities] [inst_8 : W₂.ContainsIdentities] (X₁ : C₁) (X₂ : C₂),
  ((CategoryTheory.Localization.Lifting₂.iso L₁ L₂ W₁ W₂ F (CategoryTheory.Localization.lift₂ F hF L₁ L₂)).hom.app
          X₁).app
      X₂ =
    (CategoryTheory.Localization.Lifting.iso L₁ W₁ (F.flip.obj X₂)
            ((CategoryTheory.Localization.lift₂ F hF L₁ L₂).flip.obj (L₂.obj X₂))).hom.app
      X₁