∀ {C₁ : Type u_6} {C₂ : Type u_8} {D₁ : Type u_4} {D₂ : Type u_2} [inst : CategoryTheory.Category.{u_5, u_6} C₁]
  [inst_1 : CategoryTheory.Category.{u_7, u_8} C₂] [inst_2 : CategoryTheory.Category.{u_3, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{u_1, u_2} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) {L₁ : CategoryTheory.Functor C₁ D₁} {L₂ : CategoryTheory.Functor C₂ D₂}
  (W₁ : CategoryTheory.MorphismProperty C₁) [inst_4 : L₁.IsLocalization W₁] {G' : CategoryTheory.Functor D₁ D₂}
  {F' : CategoryTheory.Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F')
  [G'.IsLeftDerivedFunctor α W₁] (η : CategoryTheory.Functor.id D₁ ⟶ G'.comp F')
  (ε : F'.comp G' ⟶ CategoryTheory.Functor.id D₂),
  (∀ (X₁ : C₁),
      CategoryTheory.CategoryStruct.comp (η.app (L₁.obj X₁)) (F'.map (α.app X₁)) =
        CategoryTheory.CategoryStruct.comp (L₁.map (adj.unit.app X₁)) (β.app (G.obj X₁))) →
    (∀ (X₂ : C₂),
        CategoryTheory.CategoryStruct.comp (G'.map (β.app X₂)) (ε.app (L₂.obj X₂)) =
          CategoryTheory.CategoryStruct.comp (α.app (F.obj X₂)) (L₂.map (adj.counit.app X₂))) →
      ∀ (X : D₁),
        CategoryTheory.CategoryStruct.comp (G'.map (η.app X)) (ε.app (G'.obj X)) =
          CategoryTheory.CategoryStruct.id (G'.obj X)