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