∀ (B : Type u_1) [inst : CategoryTheory.Bicategory B] (C : Type u_2) [inst_1 : CategoryTheory.Bicategory C]
  {a b c d : B × C} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.Prod.mkHom (CategoryTheory.Bicategory.whiskerRight η.1 (CategoryTheory.CategoryStruct.comp g h).1)
      (CategoryTheory.Bicategory.whiskerRight η.2 (CategoryTheory.CategoryStruct.comp g h).2) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Bicategory.associator f.1 g.1 h.1).prod (CategoryTheory.Bicategory.associator f.2 g.2 h.2)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Prod.mkHom
          (CategoryTheory.Bicategory.whiskerRight
            (CategoryTheory.Prod.mkHom (CategoryTheory.Bicategory.whiskerRight η.1 g.1)
                (CategoryTheory.Bicategory.whiskerRight η.2 g.2)).1
            h.1)
          (CategoryTheory.Bicategory.whiskerRight
            (CategoryTheory.Prod.mkHom (CategoryTheory.Bicategory.whiskerRight η.1 g.1)
                (CategoryTheory.Bicategory.whiskerRight η.2 g.2)).2
            h.2))
        ((CategoryTheory.Bicategory.associator f'.1 g.1 h.1).prod
            (CategoryTheory.Bicategory.associator f'.2 g.2 h.2)).hom)