∀ (B : Type u_5) [inst : CategoryTheory.Bicategory B] (C : Type u_6) [inst_1 : CategoryTheory.Bicategory C]
  {a b c d : CategoryTheory.Pseudofunctor B C} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
  CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight (CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft f η) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.StrongTrans.associator f g h).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft f
          (CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight η h))
        (CategoryTheory.Pseudofunctor.StrongTrans.associator f g' h).inv)