∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}
  {G :
    CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂)))
      (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))}
  (φ : F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂} ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp G)
  {P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))} {x y : P.Elements} (f : x ⟶ y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYoneda.{max v₂ w, v₁, u₁}.map (↑f).unop)
      (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.coconeApp φ x) =
    CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.coconeApp φ y