∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {H K : CategoryTheory.Functor B C} (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (α : H ≅ K) {Z : CategoryTheory.Functor B E} (h : (K.comp F).comp G ≅ Z),
  CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.isoWhiskerRight α F) G ≪≫ h =
    H.associator F G ≪≫ CategoryTheory.Functor.isoWhiskerRight α (F.comp G) ≪≫ (K.associator F G).symm ≪≫ h