∀ {B : Type u_5} [inst : CategoryTheory.Bicategory B] {C : Type u_3} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) (F' : F.PseudoCore) {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
  F.map₂ (CategoryTheory.Bicategory.whiskerRight η h) =
    CategoryTheory.CategoryStruct.comp (F'.mapCompIso f h).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (F.map h))
        (F'.mapCompIso g h).inv)