∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y : C} (h : X ≅ Y) (x y : CategoryTheory.Aut X),
  { hom := CategoryTheory.CategoryStruct.comp h.inv (CategoryTheory.CategoryStruct.comp (x * y).hom h.hom),
      inv := CategoryTheory.CategoryStruct.comp h.inv (CategoryTheory.CategoryStruct.comp (x * y).inv h.hom),
      hom_inv_id := ⋯, inv_hom_id := ⋯ } =
    { hom := CategoryTheory.CategoryStruct.comp h.inv (CategoryTheory.CategoryStruct.comp x.hom h.hom),
        inv := CategoryTheory.CategoryStruct.comp h.inv (CategoryTheory.CategoryStruct.comp x.inv h.hom),
        hom_inv_id := ⋯, inv_hom_id := ⋯ } *
      { hom := CategoryTheory.CategoryStruct.comp h.inv (CategoryTheory.CategoryStruct.comp y.hom h.hom),
        inv := CategoryTheory.CategoryStruct.comp h.inv (CategoryTheory.CategoryStruct.comp y.inv h.hom),
        hom_inv_id := ⋯, inv_hom_id := ⋯ }