∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y : CategoryTheory.Monad C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f.toNatTrans = CategoryTheory.MonObj.one