∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h)
  [inst_1 : CategoryTheory.IsIso η],
  CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.inv η) =
    CategoryTheory.inv (CategoryTheory.Bicategory.whiskerLeft f η)