∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F))
  (Z : CategoryTheory.Limits.WalkingParallelPair),
  (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj F U c).π.app Z =
    CategoryTheory.Limits.WalkingParallelPair.casesOn Z
      (CategoryTheory.Limits.Pi.lift fun i => c.π.app (Opposite.op (CategoryTheory.Pairwise.single i)))
      (CategoryTheory.Limits.Pi.lift fun b => c.π.app (Opposite.op (CategoryTheory.Pairwise.pair b.1 b.2)))