∀ (R : Type u_1) [inst : CommRing R] (x x_1 x_2 : HopfAlgCat R) (x_3 : x_1 ⟶ x_2),
  (CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft x x_3) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl
          (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x)
            ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x_1))).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x)
          ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).map x_3))
        (CategoryTheory.Iso.refl
            (CategoryTheory.MonoidalCategoryStruct.tensorObj
              ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x)
              ((CategoryTheory.forget₂ (HopfAlgCat R) (BialgCat R)).obj x_2))).hom)