∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) {Z : a ⟶ c}
  (h_1 : CategoryTheory.CategoryStruct.comp f h ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.inv)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.hom) h_1) =
    h_1