∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor Dᵒᵖ Eᵒᵖ} (α : F ⟶ G),
  CategoryTheory.NatTrans.unop (CategoryTheory.Functor.whiskerRight α H) =
    CategoryTheory.CategoryStruct.comp (G.unopComp H).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.unop α) H.unop)
        (F.unopComp H).inv)