∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {a b : CategoryTheory.MonoidalSingleObj C} {f g : C} (η : f ⟶ g),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight η (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor f).hom
      (CategoryTheory.CategoryStruct.comp η (CategoryTheory.MonoidalCategoryStruct.rightUnitor g).inv)