∀ (M : Type u_1) [inst : Monoid M] (W X Y Z : CategoryTheory.Discrete M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToIso ⋯).hom (CategoryTheory.eqToHom ⋯)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToIso ⋯).hom (CategoryTheory.Discrete.eqToIso ⋯).hom