∀ {B : Type u_6} [inst : CategoryTheory.Bicategory B] (b : B) (C : Type u_2) [inst_1 : CategoryTheory.Bicategory C]
  {a b_1 : C} (f : a ⟶ b_1),
  CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id b))
      (CategoryTheory.Bicategory.rightUnitor f).hom =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id b)).symm.prod
          (CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b_1)))).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id b) f)).hom)