∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁)
  (f : X ⟶ Y) (g : Y ⟶ Z),
  (α.homCongr γ) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp ((α.homCongr β) f) ((β.homCongr γ) g)