∀ (C : Type u_4) [inst : CategoryTheory.Category.{u_2, u_4} C] (D : Type u_3)
  [inst_1 : CategoryTheory.Category.{u_1, u_3} D] {X Y Z : D ≌ C} (x : X ⟶ Y) (x_1 : Y ⟶ Z),
  (CategoryTheory.Equivalence.mkHom
        ((CategoryTheory.conjugateEquiv X.symm.toAdjunction Z.symm.toAdjunction).invFun
          (CategoryTheory.Equivalence.asNatTrans (CategoryTheory.CategoryStruct.comp x x_1)))).op =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Equivalence.mkHom
          ((CategoryTheory.conjugateEquiv X.symm.toAdjunction Y.symm.toAdjunction).invFun
            (CategoryTheory.Equivalence.asNatTrans x))).op
      (CategoryTheory.Equivalence.mkHom
          ((CategoryTheory.conjugateEquiv Y.symm.toAdjunction Z.symm.toAdjunction).invFun
            (CategoryTheory.Equivalence.asNatTrans x_1))).op