∀ (B : Type u_1) [inst : CategoryTheory.Bicategory B] {a b c d : CategoryTheory.Bicategory.Pith B} (f : a ⟶ b)
  (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
  { iso := CategoryTheory.Bicategory.whiskerLeftIso (CategoryTheory.CategoryStruct.comp f g).of η.iso } =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Core.isoMk (CategoryTheory.Bicategory.associator f.of g.of h.of)).hom
      (CategoryTheory.CategoryStruct.comp
        {
          iso :=
            CategoryTheory.Bicategory.whiskerLeftIso f.of
              { iso := CategoryTheory.Bicategory.whiskerLeftIso g.of η.iso }.iso }
        (CategoryTheory.Core.isoMk (CategoryTheory.Bicategory.associator f.of g.of h'.of)).inv)