∀ (B : Type u_2) [inst : CategoryTheory.Bicategory B] {C : Type u_6} [inst_1 : CategoryTheory.Bicategory C] (c : C)
  {a b c_1 : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c_1),
  CategoryTheory.Prod.mkHom (CategoryTheory.Bicategory.whiskerRight η h)
      (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id c)) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp f h)).prod
          (CategoryTheory.Bicategory.leftUnitor (h, CategoryTheory.CategoryStruct.id c).2).symm).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight
          (CategoryTheory.Prod.mkHom η (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id c)))
          (CategoryTheory.Prod.mkHom h (CategoryTheory.CategoryStruct.id c)))
        ((CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp g h)).prod
            (CategoryTheory.Bicategory.leftUnitor (h, CategoryTheory.CategoryStruct.id c).2).symm).inv)