-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
⊢ ⋯.some.lift
        { pt := s.pt,
          π :=
            {
              app := fun (X_1 : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
                Opposite.casesOn (motive := fun (x : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
                  Functor.obj.{w, v_1, w, u_1}
                      (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) x ⟶
                    Functor.obj
                      (Functor.op
                          (Pairwise.diagram fun (j : ULift.{w, 0} WalkingPair) ↦
                            WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V) ⋙
                        F.presheaf)
                      x)
                  X_1 fun (unop : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
                  Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
                    Functor.obj.{w, v_1, w, u_1}
                        (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                        (op x) ⟶
                      Functor.obj
                        (Functor.op
                            (Pairwise.diagram fun (j : ULift.{w, 0} WalkingPair) ↦
                              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V) ⋙
                          F.presheaf)
                        (op x))
                    unop
                    (fun (a : ULift.{w, 0} WalkingPair) ↦
                      ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
                        Functor.obj.{w, v_1, w, u_1}
                            (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                            (op (Pairwise.single x)) ⟶
                          Functor.obj
                            (Functor.op
                                (Pairwise.diagram fun (j : ULift.{w, 0} WalkingPair) ↦
                                  WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U
                                    V) ⋙
                              F.presheaf)
                            (op (Pairwise.single x)))
                        a fun (down : WalkingPair) ↦
                        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                          Functor.obj.{w, v_1, w, u_1}
                              (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                              (op (Pairwise.single { down := x : ULift.{w, 0} WalkingPair })) ⟶
                            Functor.obj
                              (Functor.op
                                  (Pairwise.diagram fun (j : ULift.{w, 0} WalkingPair) ↦
                                    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U
                                      V) ⋙
                                F.presheaf)
                              (op (Pairwise.single { down := x : ULift.{w, 0} WalkingPair })))
                          down s.fst s.snd)
                    fun (a a_1 : ULift.{w, 0} WalkingPair) ↦
                    ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
                      Functor.obj.{w, v_1, w, u_1}
                          (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                          (op (Pairwise.pair x a_1)) ⟶
                        Functor.obj
                          (Functor.op
                              (Pairwise.diagram fun (j : ULift.{w, 0} WalkingPair) ↦
                                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U
                                  V) ⋙
                            F.presheaf)
                          (op (Pairwise.pair x a_1)))
                      a fun (down : WalkingPair) ↦
                      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                        Functor.obj.{w, v_1, w, u_1}
                            (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                            (op (Pairwise.pair { down := x : ULift.{w, 0} WalkingPair } a_1)) ⟶
                          Functor.obj
                            (Functor.op
                                (Pairwise.diagram fun (j : ULift.{w, 0} WalkingPair) ↦
                                  WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U
                                    V) ⋙
                              F.presheaf)
                            (op (Pairwise.pair { down := x : ULift.{w, 0} WalkingPair } a_1)))
                        down
                        (s.fst ≫
                          F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                            (homOfLE ⋯).op)
                        (s.snd ≫
                          F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                            (homOfLE ⋯).op),
              naturality := ⋯ :
              NatTrans (C := (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ)
                (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                (Functor.op
                    (Pairwise.diagram fun (j : ULift.{w, 0} WalkingPair) ↦
                      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V) ⋙
                  F.presheaf) } } ≫
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
        (Quiver.Hom.op (eqToHom ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)) =
    s.snd

Tactic:
exact
    (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 _).some.fac _ <|
      op <| Pairwise.single <| ULift.up WalkingPair.right

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections, CategoryTheory.Limits.WalkingPair.right, Nonempty.some, CategoryTheory.Pairwise.single, Opposite.op, Iff.mp, TopCat.Sheaf.presheaf, ULift.up, CategoryTheory.Limits.IsLimit.fac