∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_7, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_8, u_2} D] {E : Type u_5} [inst_2 : CategoryTheory.Category.{u_3, u_5} E]
  {E' : Type u_6} [inst_3 : CategoryTheory.Category.{u_4, u_6} E'] (H : CategoryTheory.Functor C E)
  {Fᵣ Gᵣ : CategoryTheory.Functor D E'} (α : Fᵣ ⟶ Gᵣ),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) (CategoryTheory.Join.mapPair H Fᵣ))
      ((CategoryTheory.Prod.snd C D).whiskerLeft
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapPairRight H Fᵣ).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.whiskerRight α (CategoryTheory.Join.inclRight E E'))
            (CategoryTheory.Join.mapPairRight H Gᵣ).inv))) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Prod.fst C D).whiskerLeft
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapPairLeft H Fᵣ).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.whiskerRight (CategoryTheory.CategoryStruct.id H)
              (CategoryTheory.Join.inclLeft E E'))
            (CategoryTheory.Join.mapPairLeft H Gᵣ).inv)))
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) (CategoryTheory.Join.mapPair H Gᵣ))