∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] (x : CategoryTheory.Mon (CategoryTheory.Functor C C)),
  CategoryTheory.IsMonHom
    (CategoryTheory.CategoryStruct.id
      (((CategoryTheory.Monad.monToMonad C).comp (CategoryTheory.Monad.monadToMon C)).obj x).X)