∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {M N : CategoryTheory.Monad C}
  (f : M.toFunctor ≅ N.toFunctor),
  (∀ (X : C),
      CategoryTheory.CategoryStruct.comp (M.μ.app X) (f.hom.app X) =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CategoryStruct.comp (M.map (f.hom.app X)) (f.hom.app (N.obj X))) (N.μ.app X)) →
    ∀ (X : C),
      CategoryTheory.CategoryStruct.comp (N.μ.app X) (f.inv.app X) =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CategoryStruct.comp (N.map (f.inv.app X)) (f.inv.app (M.obj X))) (M.μ.app X)