∀ (F : Type u_1 → Type u_2) [inst : Applicative F] [inst_1 : LawfulApplicative F] {X Y : Type u_1} (f : X ⟶ Y)
  (X' : Type u_1),
  (CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((CategoryTheory.ofTypeFunctor F).map f)
        ((CategoryTheory.ofTypeFunctor F).obj X'))
      fun p => Prod.mk <$> p.1 <*> p.2) =
    CategoryTheory.CategoryStruct.comp (fun p => Prod.mk <$> p.1 <*> p.2)
      ((CategoryTheory.ofTypeFunctor F).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X'))