∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] {iC : CategoryTheory.Functor C C'} {iD : CategoryTheory.Functor D D'}
  {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful)
  (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}
  (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) (X : D),
  iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X) =
    CategoryTheory.CategoryStruct.comp (comm1.inv.app (R.obj X))
      (CategoryTheory.CategoryStruct.comp (L'.map (comm2.inv.app X)) (adj.counit.app (iD.obj X)))