C : Type u
inst✝ : Category C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
⊢ IsLimit.lift
        (Nonempty.some
          (_ :
            Nonempty
              (IsLimit ((presheaf F).mapCone (Cocone.op (Pairwise.cocone fun j => WalkingPair.casesOn j.down U V))))))
        { pt := s.pt,
          π :=
            NatTrans.mk fun X_1 =>
              Opposite.casesOn X_1 fun unop =>
                Pairwise.casesOn unop
                  (fun a =>
                    ULift.casesOn a fun down => WalkingPair.casesOn down (PullbackCone.fst s) (PullbackCone.snd s))
                  fun a a_1 =>
                  ULift.casesOn a fun down =>
                    WalkingPair.casesOn down
                      (PullbackCone.fst s ≫
                        F.val.map (homOfLE (_ : U ⊓ (fun j => WalkingPair.casesOn j.down U V) a_1 ≤ U)).op)
                      (PullbackCone.snd s ≫
                        F.val.map (homOfLE (_ : V ⊓ (fun j => WalkingPair.casesOn j.down U V) a_1 ≤ V)).op) } ≫
      F.val.map (eqToHom (_ : U ⊔ V = ⨆ (j : ULift WalkingPair), WalkingPair.casesOn j.down U V)).op ≫
        F.val.map (homOfLE (_ : U ≤ U ⊔ V)).op =
    PullbackCone.fst s
C : Type u
inst✝ : Category C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
⊢ interUnionPullbackConeLift F U V s ≫ F.val.map (homOfLE (_ : U ≤ U ⊔ V)).op = PullbackCone.fst s
erw [Category.assoc]
C : Type u
inst✝ : Category C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
⊢ IsLimit.lift
        (Nonempty.some
          (_ :
            Nonempty
              (IsLimit ((presheaf F).mapCone (Cocone.op (Pairwise.cocone fun j => WalkingPair.casesOn j.down U V))))))
        { pt := s.pt,
          π :=
            NatTrans.mk fun X_1 =>
              Pairwise.rec (fun a => WalkingPair.rec (PullbackCone.fst s) (PullbackCone.snd s) a.down)
                (fun a a_1 =>
                  WalkingPair.rec
                    (PullbackCone.fst s ≫ F.val.map (homOfLE (_ : U ⊓ WalkingPair.rec U V a_1.down ≤ U)).op)
                    (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ WalkingPair.rec U V a_1.down ≤ V)).op) a.down)
                X_1.unop } ≫
      F.val.map
        ((eqToHom (_ : U ⊔ V = ⨆ (j : ULift WalkingPair), WalkingPair.casesOn j.down U V)).op ≫
          (homOfLE (_ : U ≤ U ⊔ V)).op) =
    PullbackCone.fst s
C : Type u
inst✝ : Category C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
⊢ IsLimit.lift
        (Nonempty.some
          (_ :
            Nonempty
              (IsLimit ((presheaf F).mapCone (Cocone.op (Pairwise.cocone fun j => WalkingPair.casesOn j.down U V))))))
        { pt := s.pt,
          π :=
            NatTrans.mk fun X_1 =>
              Opposite.casesOn X_1 fun unop =>
                Pairwise.casesOn unop
                  (fun a =>
                    ULift.casesOn a fun down => WalkingPair.casesOn down (PullbackCone.fst s) (PullbackCone.snd s))
                  fun a a_1 =>
                  ULift.casesOn a fun down =>
                    WalkingPair.casesOn down
                      (PullbackCone.fst s ≫
                        F.val.map (homOfLE (_ : U ⊓ (fun j => WalkingPair.casesOn j.down U V) a_1 ≤ U)).op)
                      (PullbackCone.snd s ≫
                        F.val.map (homOfLE (_ : V ⊓ (fun j => WalkingPair.casesOn j.down U V) a_1 ≤ V)).op) } ≫
      F.val.map (eqToHom (_ : U ⊔ V = ⨆ (j : ULift WalkingPair), WalkingPair.casesOn j.down U V)).op ≫
        F.val.map (homOfLE (_ : U ≤ U ⊔ V)).op =
    PullbackCone.fst s
simp_rw [← F.1.map_comp]
no goals
C : Type u
inst✝ : Category C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
⊢ IsLimit.lift
        (Nonempty.some
          (_ :
            Nonempty
              (IsLimit ((presheaf F).mapCone (Cocone.op (Pairwise.cocone fun j => WalkingPair.casesOn j.down U V))))))
        { pt := s.pt,
          π :=
            NatTrans.mk fun X_1 =>
              Pairwise.rec (fun a => WalkingPair.rec (PullbackCone.fst s) (PullbackCone.snd s) a.down)
                (fun a a_1 =>
                  WalkingPair.rec
                    (PullbackCone.fst s ≫ F.val.map (homOfLE (_ : U ⊓ WalkingPair.rec U V a_1.down ≤ U)).op)
                    (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ WalkingPair.rec U V a_1.down ≤ V)).op) a.down)
                X_1.unop } ≫
      F.val.map
        ((eqToHom (_ : U ⊔ V = ⨆ (j : ULift WalkingPair), WalkingPair.casesOn j.down U V)).op ≫
          (homOfLE (_ : U ≤ U ⊔ V)).op) =
    PullbackCone.fst s
exact
  (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 _).some.fac _ <|
    op <| Pairwise.single <| ULift.up WalkingPair.left