∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C],
  CategoryTheory.CategoryStruct.comp
      {
        app := fun x =>
          {
            hom :=
              CategoryTheory.CategoryStruct.id
                ((CategoryTheory.Functor.id (CategoryTheory.Mon (CategoryTheory.Functor C C))).obj x).X,
            isMonHom_hom := ⋯ },
        naturality := ⋯ }
      {
        app := fun x =>
          {
            hom :=
              CategoryTheory.CategoryStruct.id
                (((CategoryTheory.Monad.monToMonad C).comp (CategoryTheory.Monad.monadToMon C)).obj x).X,
            isMonHom_hom := ⋯ },
        naturality := ⋯ } =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.id (CategoryTheory.Mon (CategoryTheory.Functor C C)))