∀ {C : Type u_5} [inst : CategoryTheory.Category.{u_6, u_5} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{u_4, u_1} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{u_2, u_3} E]
  (e : C ≌ D) (F : CategoryTheory.Functor C E),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.whiskeringLeft D C E).obj e.inverse).map
        ((CategoryTheory.NatIso.ofComponents (fun F => (e.funInvIdAssoc F).symm) ⋯).hom.app F))
      ((CategoryTheory.NatIso.ofComponents (fun F => e.invFunIdAssoc F) ⋯).hom.app
        (((CategoryTheory.Functor.whiskeringLeft D C E).obj e.inverse).obj F)) =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.whiskeringLeft D C E).obj e.inverse).obj F)