∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {A : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_3, u_4} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  [inst_3 : CategoryTheory.Limits.HasPullbacks C] (P : CategoryTheory.Functor Cᵒᵖ A)
  (s : CategoryTheory.Functor A (Type (max u_2 u_1)))
  [inst_4 : ∀ (J : Type (max u_2 u_1)), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) s]
  (U : C) (R : CategoryTheory.Presieve U),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Limits.parallelPair (s.map (CategoryTheory.Presheaf.firstMap R P))
            (s.map (CategoryTheory.Presheaf.secondMap R P))).map
        CategoryTheory.Limits.WalkingParallelPairHom.right)
      (CategoryTheory.Limits.PreservesProduct.iso s fun fg =>
          P.obj (Opposite.op (CategoryTheory.Limits.pullback ↑fg.1.snd ↑fg.2.snd))).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.PreservesProduct.iso s fun f => P.obj (Opposite.op f.fst)).hom
      ((CategoryTheory.Limits.parallelPair (CategoryTheory.Equalizer.Presieve.firstMap (P.comp s) R)
            (CategoryTheory.Equalizer.Presieve.secondMap (P.comp s) R)).map
        CategoryTheory.Limits.WalkingParallelPairHom.right)