∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) (X : ↑(self.obj a)) {Z : ↑(self.obj c)}
  (h_1 : (self.map (CategoryTheory.CategoryStruct.comp f h)).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)).toNatTrans.app X) h_1 =
    CategoryTheory.CategoryStruct.comp ((self.mapComp f g).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X))
        (CategoryTheory.CategoryStruct.comp ((self.mapComp f h).inv.toNatTrans.app X) h_1))