∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] (E : Type u_5) [inst_2 : CategoryTheory.Category.{u_6, u_5} E]
  {X Y Z : C ≌ D} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Equivalence.mkHom
      ((CategoryTheory.Functor.whiskeringRight E C D).map
        (CategoryTheory.Equivalence.asNatTrans (CategoryTheory.CategoryStruct.comp f g))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Equivalence.mkHom
        ((CategoryTheory.Functor.whiskeringRight E C D).map (CategoryTheory.Equivalence.asNatTrans f)))
      (CategoryTheory.Equivalence.mkHom
        ((CategoryTheory.Functor.whiskeringRight E C D).map (CategoryTheory.Equivalence.asNatTrans g)))