∀ {A : Type u_1} {B : Type u_2} (C : Type u_3) [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor A B),
  CategoryTheory.Join.mapWhiskerRight F.rightUnitor.hom (CategoryTheory.Functor.id C) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompLeft C F (CategoryTheory.Functor.id B)).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Join.mapPair F (CategoryTheory.Functor.id C)).whiskerLeft CategoryTheory.Join.mapPairId.hom)
        (CategoryTheory.Join.mapPair F (CategoryTheory.Functor.id C)).rightUnitor.hom)