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