[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
V : OpensLeCover U
A B : StructuredArrow V (pairwiseToOpensLeCover U)
⊢ ∃ l, List.Chain Zag A l ∧ List.getLast (A :: l) (_ : A :: l ≠ []) = B
[PROOFSTEP]
rcases A with ⟨⟨⟨⟩⟩, ⟨i⟩ | ⟨i, j⟩, a⟩
[GOAL]
case mk.mk.unit.single
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
V : OpensLeCover U
B : StructuredArrow V (pairwiseToOpensLeCover U)
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
⊢ ∃ l,
    List.Chain Zag { left := { as := PUnit.unit }, right := single i, hom := a } l ∧
      List.getLast ({ left := { as := PUnit.unit }, right := single i, hom := a } :: l)
          (_ : { left := { as := PUnit.unit }, right := single i, hom := a } :: l ≠ []) =
        B
[PROOFSTEP]
rcases B with ⟨⟨⟨⟩⟩, ⟨i'⟩ | ⟨i', j'⟩, b⟩
[GOAL]
case mk.mk.unit.pair
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
V : OpensLeCover U
B : StructuredArrow V (pairwiseToOpensLeCover U)
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
⊢ ∃ l,
    List.Chain Zag { left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } l ∧
      List.getLast ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l)
          (_ : { left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l ≠ []) =
        B
[PROOFSTEP]
rcases B with ⟨⟨⟨⟩⟩, ⟨i'⟩ | ⟨i', j'⟩, b⟩
[GOAL]
case mk.mk.unit.single.mk.mk.unit.single
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ∃ l,
    List.Chain Zag { left := { as := PUnit.unit }, right := single i, hom := a } l ∧
      List.getLast ({ left := { as := PUnit.unit }, right := single i, hom := a } :: l)
          (_ : { left := { as := PUnit.unit }, right := single i, hom := a } :: l ≠ []) =
        { left := { as := PUnit.unit }, right := single i', hom := b }
[PROOFSTEP]
refine'
  ⟨[{   left := ⟨⟨⟩⟩
        right := pair i i'
        hom := (le_inf a.le b.le).hom }, _], _, rfl⟩
[GOAL]
case mk.mk.unit.single.mk.mk.unit.single
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ List.Chain Zag { left := { as := PUnit.unit }, right := single i, hom := a }
    [{ left := { as := PUnit.unit }, right := Pairwise.pair i i',
        hom :=
          LE.le.hom
            (_ :
              ((Functor.fromPUnit V).obj { as := PUnit.unit }).obj ≤
                ((pairwiseToOpensLeCover U).obj (single i)).obj ⊓ ((pairwiseToOpensLeCover U).obj (single i')).obj) },
      { left := { as := PUnit.unit }, right := single i', hom := b }]
[PROOFSTEP]
exact
  List.Chain.cons
    (Or.inr
      ⟨{  left := 𝟙 _
          right := left i i' }⟩)
    (List.Chain.cons
      (Or.inl
        ⟨{  left := 𝟙 _
            right := right i i' }⟩)
      List.Chain.nil)
[GOAL]
case mk.mk.unit.single.mk.mk.unit.pair
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ∃ l,
    List.Chain Zag { left := { as := PUnit.unit }, right := single i, hom := a } l ∧
      List.getLast ({ left := { as := PUnit.unit }, right := single i, hom := a } :: l)
          (_ : { left := { as := PUnit.unit }, right := single i, hom := a } :: l ≠ []) =
        { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }
[PROOFSTEP]
refine'
  ⟨[{   left := ⟨⟨⟩⟩
        right := pair i' i
        hom := (le_inf (b.le.trans inf_le_left) a.le).hom },
      { left := ⟨⟨⟩⟩
        right := single i'
        hom := (b.le.trans inf_le_left).hom }, _], _, rfl⟩
[GOAL]
case mk.mk.unit.single.mk.mk.unit.pair
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ List.Chain Zag { left := { as := PUnit.unit }, right := single i, hom := a }
    [{ left := { as := PUnit.unit }, right := Pairwise.pair i' i,
        hom :=
          LE.le.hom
            (_ :
              ((Functor.fromPUnit V).obj { as := PUnit.unit }).obj ≤
                U i' ⊓ ((pairwiseToOpensLeCover U).obj (single i)).obj) },
      { left := { as := PUnit.unit }, right := single i',
        hom := LE.le.hom (_ : ((Functor.fromPUnit V).obj { as := PUnit.unit }).obj ≤ U i') },
      { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }]
[PROOFSTEP]
exact
  List.Chain.cons
    (Or.inr
      ⟨{  left := 𝟙 _
          right := right i' i }⟩)
    (List.Chain.cons
      (Or.inl
        ⟨{  left := 𝟙 _
            right := left i' i }⟩)
      (List.Chain.cons
        (Or.inr
          ⟨{  left := 𝟙 _
              right := left i' j' }⟩)
        List.Chain.nil))
[GOAL]
case mk.mk.unit.pair.mk.mk.unit.single
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ∃ l,
    List.Chain Zag { left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } l ∧
      List.getLast ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l)
          (_ : { left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l ≠ []) =
        { left := { as := PUnit.unit }, right := single i', hom := b }
[PROOFSTEP]
refine'
  ⟨[{   left := ⟨⟨⟩⟩
        right := single i
        hom := (a.le.trans inf_le_left).hom },
      { left := ⟨⟨⟩⟩
        right := pair i i'
        hom := (le_inf (a.le.trans inf_le_left) b.le).hom }, _], _, rfl⟩
[GOAL]
case mk.mk.unit.pair.mk.mk.unit.single
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ List.Chain Zag { left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a }
    [{ left := { as := PUnit.unit }, right := single i,
        hom := LE.le.hom (_ : ((Functor.fromPUnit V).obj { as := PUnit.unit }).obj ≤ U i) },
      { left := { as := PUnit.unit }, right := Pairwise.pair i i',
        hom :=
          LE.le.hom
            (_ :
              ((Functor.fromPUnit V).obj { as := PUnit.unit }).obj ≤
                U i ⊓ ((pairwiseToOpensLeCover U).obj (single i')).obj) },
      { left := { as := PUnit.unit }, right := single i', hom := b }]
[PROOFSTEP]
exact
  List.Chain.cons
    (Or.inl
      ⟨{  left := 𝟙 _
          right := left i j }⟩)
    (List.Chain.cons
      (Or.inr
        ⟨{  left := 𝟙 _
            right := left i i' }⟩)
      (List.Chain.cons
        (Or.inl
          ⟨{  left := 𝟙 _
              right := right i i' }⟩)
        List.Chain.nil))
[GOAL]
case mk.mk.unit.pair.mk.mk.unit.pair
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ∃ l,
    List.Chain Zag { left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } l ∧
      List.getLast ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l)
          (_ : { left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l ≠ []) =
        { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }
[PROOFSTEP]
refine'
  ⟨[{   left := ⟨⟨⟩⟩
        right := single i
        hom := (a.le.trans inf_le_left).hom },
      { left := ⟨⟨⟩⟩
        right := pair i i'
        hom := (le_inf (a.le.trans inf_le_left) (b.le.trans inf_le_left)).hom },
      { left := ⟨⟨⟩⟩
        right := single i'
        hom := (b.le.trans inf_le_left).hom }, _], _, rfl⟩
[GOAL]
case mk.mk.unit.pair.mk.mk.unit.pair
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ List.Chain Zag { left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a }
    [{ left := { as := PUnit.unit }, right := single i,
        hom := LE.le.hom (_ : ((Functor.fromPUnit V).obj { as := PUnit.unit }).obj ≤ U i) },
      { left := { as := PUnit.unit }, right := Pairwise.pair i i',
        hom := LE.le.hom (_ : ((Functor.fromPUnit V).obj { as := PUnit.unit }).obj ≤ U i ⊓ U i') },
      { left := { as := PUnit.unit }, right := single i',
        hom := LE.le.hom (_ : ((Functor.fromPUnit V).obj { as := PUnit.unit }).obj ≤ U i') },
      { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }]
[PROOFSTEP]
exact
  List.Chain.cons
    (Or.inl
      ⟨{  left := 𝟙 _
          right := left i j }⟩)
    (List.Chain.cons
      (Or.inr
        ⟨{  left := 𝟙 _
            right := left i i' }⟩)
      (List.Chain.cons
        (Or.inl
          ⟨{  left := 𝟙 _
              right := right i i' }⟩)
        (List.Chain.cons
          (Or.inr
            ⟨{  left := 𝟙 _
                right := left i' j' }⟩)
          List.Chain.nil)))
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
⊢ (X_1 : CategoryTheory.Pairwise ι) →
    (diagram U).obj X_1 ⟶ (pairwiseToOpensLeCover U ⋙ fullSubcategoryInclusion fun V => ∃ i, V ≤ U i).obj X_1
[PROOFSTEP]
rintro (i | ⟨i, j⟩)
[GOAL]
case single
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
i : ι
⊢ (diagram U).obj (single i) ⟶
    (pairwiseToOpensLeCover U ⋙ fullSubcategoryInclusion fun V => ∃ i, V ≤ U i).obj (single i)
[PROOFSTEP]
exact 𝟙 _
[GOAL]
case pair
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
i j : ι
⊢ (diagram U).obj (Pairwise.pair i j) ⟶
    (pairwiseToOpensLeCover U ⋙ fullSubcategoryInclusion fun V => ∃ i, V ≤ U i).obj (Pairwise.pair i j)
[PROOFSTEP]
exact 𝟙 _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
⊢ (X_1 : CategoryTheory.Pairwise ι) →
    (pairwiseToOpensLeCover U ⋙ fullSubcategoryInclusion fun V => ∃ i, V ≤ U i).obj X_1 ⟶ (diagram U).obj X_1
[PROOFSTEP]
rintro (i | ⟨i, j⟩)
[GOAL]
case single
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
i : ι
⊢ (pairwiseToOpensLeCover U ⋙ fullSubcategoryInclusion fun V => ∃ i, V ≤ U i).obj (single i) ⟶
    (diagram U).obj (single i)
[PROOFSTEP]
exact 𝟙 _
[GOAL]
case pair
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
i j : ι
⊢ (pairwiseToOpensLeCover U ⋙ fullSubcategoryInclusion fun V => ∃ i, V ≤ U i).obj (Pairwise.pair i j) ⟶
    (diagram U).obj (Pairwise.pair i j)
[PROOFSTEP]
exact 𝟙 _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type w
U : ι → Opens ↑X
⊢ ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
    NatTrans.app (Cocone.op (cocone U)).π j =
      (Iso.refl (Cocone.op (cocone U)).pt).hom ≫
        NatTrans.app
          ((Cones.postcomposeEquivalence (NatIso.op (pairwiseDiagramIso U))).functor.obj
              (Cone.whisker (pairwiseToOpensLeCover U).op (Cocone.op (opensLeCoverCocone U)))).π
          j
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
⊢ IsSheaf F ↔ IsSheafPairwiseIntersections F
[PROOFSTEP]
rw [isSheaf_iff_isSheafOpensLeCover, isSheafOpensLeCover_iff_isSheafPairwiseIntersections]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
⊢ IsSheaf F ↔ IsSheafPreservesLimitPairwiseIntersections F
[PROOFSTEP]
rw [isSheaf_iff_isSheafPairwiseIntersections]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
⊢ IsSheafPairwiseIntersections F ↔ IsSheafPreservesLimitPairwiseIntersections F
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
⊢ IsSheafPairwiseIntersections F → IsSheafPreservesLimitPairwiseIntersections F
[PROOFSTEP]
intro h ι U
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty (PreservesLimit (Pairwise.diagram U).op F)
[PROOFSTEP]
exact ⟨preservesLimitOfPreservesLimitCone (Pairwise.coconeIsColimit U).op (h U).some⟩
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
⊢ IsSheafPreservesLimitPairwiseIntersections F → IsSheafPairwiseIntersections F
[PROOFSTEP]
intro h ι U
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
h : IsSheafPreservesLimitPairwiseIntersections F
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (Pairwise.cocone U))))
[PROOFSTEP]
haveI := (h U).some
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
h : IsSheafPreservesLimitPairwiseIntersections F
ι : Type w
U : ι → Opens ↑X
this : PreservesLimit (Pairwise.diagram U).op F
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (Pairwise.cocone U))))
[PROOFSTEP]
exact ⟨PreservesLimit.preserves (Pairwise.coconeIsColimit U).op⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
⊢ F.val.map (homOfLE (_ : U ≤ U ⊔ V)).op ≫ F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op =
    F.val.map (homOfLE (_ : V ≤ U ⊔ V)).op ≫ F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op
[PROOFSTEP]
rw [← F.1.map_comp, ← F.1.map_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
⊢ F.val.map ((homOfLE (_ : U ≤ U ⊔ V)).op ≫ (homOfLE (_ : U ⊓ V ≤ U)).op) =
    F.val.map ((homOfLE (_ : V ≤ U ⊔ V)).op ≫ (homOfLE (_ : U ⊓ V ≤ V)).op)
[PROOFSTEP]
congr 1
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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)
⊢ s.pt ⟶ F.val.obj (op (U ⊔ V))
[PROOFSTEP]
let ι : ULift.{w} WalkingPair → Opens X := fun j => WalkingPair.casesOn j.down U V
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
⊢ s.pt ⟶ F.val.obj (op (U ⊔ V))
[PROOFSTEP]
have hι : U ⊔ V = iSup ι := by
  ext
  rw [Opens.coe_iSup, Set.mem_iUnion]
  constructor
  · rintro (h | h)
    exacts [⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩]
  · rintro ⟨⟨_ | _⟩, h⟩
    exacts [Or.inl h, Or.inr h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
⊢ U ⊔ V = iSup ι
[PROOFSTEP]
ext
[GOAL]
case h.h
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) ↔ x✝ ∈ ↑(iSup ι)
[PROOFSTEP]
rw [Opens.coe_iSup, Set.mem_iUnion]
[GOAL]
case h.h
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) ↔ ∃ i, x✝ ∈ ↑(WalkingPair.casesOn i.down U V)
[PROOFSTEP]
constructor
[GOAL]
case h.h.mp
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) → ∃ i, x✝ ∈ ↑(WalkingPair.casesOn i.down U V)
[PROOFSTEP]
rintro (h | h)
[GOAL]
case h.h.mp.inl
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
x✝ : ↑X
h : x✝ ∈ ↑U
⊢ ∃ i, x✝ ∈ ↑(WalkingPair.casesOn i.down U V)
case h.h.mp.inr
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
x✝ : ↑X
h : x✝ ∈ ↑V
⊢ ∃ i, x✝ ∈ ↑(WalkingPair.casesOn i.down U V)
[PROOFSTEP]
exacts [⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩]
[GOAL]
case h.h.mpr
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
x✝ : ↑X
⊢ (∃ i, x✝ ∈ ↑(WalkingPair.casesOn i.down U V)) → x✝ ∈ ↑(U ⊔ V)
[PROOFSTEP]
rintro ⟨⟨_ | _⟩, h⟩
[GOAL]
case h.h.mpr.intro.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
x✝ : ↑X
h : x✝ ∈ ↑(WalkingPair.casesOn { down := WalkingPair.left }.down U V)
⊢ x✝ ∈ ↑(U ⊔ V)
case h.h.mpr.intro.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
x✝ : ↑X
h : x✝ ∈ ↑(WalkingPair.casesOn { down := WalkingPair.right }.down U V)
⊢ x✝ ∈ ↑(U ⊔ V)
[PROOFSTEP]
exacts [Or.inl h, Or.inr h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ s.pt ⟶ F.val.obj (op (U ⊔ V))
[PROOFSTEP]
refine'
  (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 ι).some.lift
      ⟨s.pt,
        { app := _
          naturality := _ }⟩ ≫
    F.1.map (eqToHom hι).op
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ (X_1 : (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ) →
    ((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).obj X_1 ⟶
      ((Pairwise.diagram ι).op ⋙ presheaf F).obj X_1
[PROOFSTEP]
rintro ((_ | _) | (_ | _))
[GOAL]
case refine'_1.mk.single.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ ((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).obj
      { unop := Pairwise.single { down := WalkingPair.left } } ⟶
    ((Pairwise.diagram ι).op ⋙ presheaf F).obj { unop := Pairwise.single { down := WalkingPair.left } }
case refine'_1.mk.single.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ ((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).obj
      { unop := Pairwise.single { down := WalkingPair.right } } ⟶
    ((Pairwise.diagram ι).op ⋙ presheaf F).obj { unop := Pairwise.single { down := WalkingPair.right } }
case refine'_1.mk.pair.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
a✝ : ULift WalkingPair
⊢ ((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).obj
      { unop := Pairwise.pair { down := WalkingPair.left } a✝ } ⟶
    ((Pairwise.diagram ι).op ⋙ presheaf F).obj { unop := Pairwise.pair { down := WalkingPair.left } a✝ }
case refine'_1.mk.pair.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
a✝ : ULift WalkingPair
⊢ ((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).obj
      { unop := Pairwise.pair { down := WalkingPair.right } a✝ } ⟶
    ((Pairwise.diagram ι).op ⋙ presheaf F).obj { unop := Pairwise.pair { down := WalkingPair.right } a✝ }
[PROOFSTEP]
exacts [s.fst, s.snd, s.fst ≫ F.1.map (homOfLE inf_le_left).op, s.snd ≫ F.1.map (homOfLE inf_le_left).op]
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ ∀ ⦃X_1 Y : (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ⦄ (f : X_1 ⟶ Y),
    (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map f ≫
        Opposite.casesOn Y 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 ⊓ ι a_1 ≤ U)).op)
                (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
      (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 ⊓ ι a_1 ≤ U)).op)
                (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
        ((Pairwise.diagram ι).op ⋙ presheaf F).map f
[PROOFSTEP]
rintro ⟨i⟩ ⟨j⟩ f
[GOAL]
case refine'_2.mk.mk
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
i j : CategoryTheory.Pairwise (ULift WalkingPair)
f : { unop := i } ⟶ { unop := j }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map f ≫
      Opposite.casesOn { unop := j } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := i } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map f
[PROOFSTEP]
let g : j ⟶ i := f.unop
[GOAL]
case refine'_2.mk.mk
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
i j : CategoryTheory.Pairwise (ULift WalkingPair)
f : { unop := i } ⟶ { unop := j }
g : j ⟶ i := f.unop
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map f ≫
      Opposite.casesOn { unop := j } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := i } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map f
[PROOFSTEP]
have : f = g.op := rfl
[GOAL]
case refine'_2.mk.mk
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
i j : CategoryTheory.Pairwise (ULift WalkingPair)
f : { unop := i } ⟶ { unop := j }
g : j ⟶ i := f.unop
this : f = g.op
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map f ≫
      Opposite.casesOn { unop := j } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := i } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map f
[PROOFSTEP]
clear_value g
[GOAL]
case refine'_2.mk.mk
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
i j : CategoryTheory.Pairwise (ULift WalkingPair)
f : { unop := i } ⟶ { unop := j }
g : j ⟶ i
this : f = g.op
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map f ≫
      Opposite.casesOn { unop := j } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := i } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map f
[PROOFSTEP]
subst this
[GOAL]
case refine'_2.mk.mk
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
i j : CategoryTheory.Pairwise (ULift WalkingPair)
g : j ⟶ i
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := j } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := i } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases i with (⟨⟨_ | _⟩⟩ | ⟨⟨_ | _⟩, ⟨_⟩⟩)
[GOAL]
case refine'_2.mk.mk.single.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
j : CategoryTheory.Pairwise (ULift WalkingPair)
g : j ⟶ Pairwise.single { down := WalkingPair.left }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := j } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases j with (⟨⟨_ | _⟩⟩ | ⟨⟨_ | _⟩, ⟨_⟩⟩)
[GOAL]
case refine'_2.mk.mk.single.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
j : CategoryTheory.Pairwise (ULift WalkingPair)
g : j ⟶ Pairwise.single { down := WalkingPair.right }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := j } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases j with (⟨⟨_ | _⟩⟩ | ⟨⟨_ | _⟩, ⟨_⟩⟩)
[GOAL]
case refine'_2.mk.mk.pair.up.left.up
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
j : CategoryTheory.Pairwise (ULift WalkingPair)
down✝ : WalkingPair
g : j ⟶ Pairwise.pair { down := WalkingPair.left } { down := down✝ }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := j } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.left } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases j with (⟨⟨_ | _⟩⟩ | ⟨⟨_ | _⟩, ⟨_⟩⟩)
[GOAL]
case refine'_2.mk.mk.pair.up.right.up
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
j : CategoryTheory.Pairwise (ULift WalkingPair)
down✝ : WalkingPair
g : j ⟶ Pairwise.pair { down := WalkingPair.right } { down := down✝ }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := j } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.right } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases j with (⟨⟨_ | _⟩⟩ | ⟨⟨_ | _⟩, ⟨_⟩⟩)
[GOAL]
case refine'_2.mk.mk.single.up.left.single.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
g : Pairwise.single { down := WalkingPair.left } ⟶ Pairwise.single { down := WalkingPair.left }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.single.up.left.single.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
g : Pairwise.single { down := WalkingPair.right } ⟶ Pairwise.single { down := WalkingPair.left }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.single.up.left.pair.up.left.up
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
g : Pairwise.pair { down := WalkingPair.left } { down := down✝ } ⟶ Pairwise.single { down := WalkingPair.left }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.left } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.single.up.left.pair.up.right.up
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
g : Pairwise.pair { down := WalkingPair.right } { down := down✝ } ⟶ Pairwise.single { down := WalkingPair.left }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.right } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.single.up.right.single.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
g : Pairwise.single { down := WalkingPair.left } ⟶ Pairwise.single { down := WalkingPair.right }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.single.up.right.single.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
g : Pairwise.single { down := WalkingPair.right } ⟶ Pairwise.single { down := WalkingPair.right }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.single.up.right.pair.up.left.up
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
g : Pairwise.pair { down := WalkingPair.left } { down := down✝ } ⟶ Pairwise.single { down := WalkingPair.right }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.left } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.single.up.right.pair.up.right.up
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
g : Pairwise.pair { down := WalkingPair.right } { down := down✝ } ⟶ Pairwise.single { down := WalkingPair.right }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.right } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.pair.up.left.up.single.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
g : Pairwise.single { down := WalkingPair.left } ⟶ Pairwise.pair { down := WalkingPair.left } { down := down✝ }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.left } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.pair.up.left.up.single.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
g : Pairwise.single { down := WalkingPair.right } ⟶ Pairwise.pair { down := WalkingPair.left } { down := down✝ }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.left } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.pair.up.left.up.pair.up.left.up
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝¹ down✝ : WalkingPair
g :
  Pairwise.pair { down := WalkingPair.left } { down := down✝ } ⟶
    Pairwise.pair { down := WalkingPair.left } { down := down✝¹ }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.left } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.left } { down := down✝¹ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.pair.up.left.up.pair.up.right.up
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝¹ down✝ : WalkingPair
g :
  Pairwise.pair { down := WalkingPair.right } { down := down✝ } ⟶
    Pairwise.pair { down := WalkingPair.left } { down := down✝¹ }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.right } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.left } { down := down✝¹ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.pair.up.right.up.single.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
g : Pairwise.single { down := WalkingPair.left } ⟶ Pairwise.pair { down := WalkingPair.right } { down := down✝ }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.right } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.pair.up.right.up.single.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
g : Pairwise.single { down := WalkingPair.right } ⟶ Pairwise.pair { down := WalkingPair.right } { down := down✝ }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.right } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.pair.up.right.up.pair.up.left.up
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝¹ down✝ : WalkingPair
g :
  Pairwise.pair { down := WalkingPair.left } { down := down✝ } ⟶
    Pairwise.pair { down := WalkingPair.right } { down := down✝¹ }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.left } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.right } { down := down✝¹ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.pair.up.right.up.pair.up.right.up
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝¹ down✝ : WalkingPair
g :
  Pairwise.pair { down := WalkingPair.right } { down := down✝ } ⟶
    Pairwise.pair { down := WalkingPair.right } { down := down✝¹ }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.right } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.right } { down := down✝¹ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map g.op
[PROOFSTEP]
rcases g with ⟨⟩
[GOAL]
case refine'_2.mk.mk.single.up.left.single.up.left.id_single
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map
        (Pairwise.Hom.id_single { down := WalkingPair.left }).op ≫
      Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map (Pairwise.Hom.id_single { down := WalkingPair.left }).op
[PROOFSTEP]
dsimp [Pairwise.diagram]
[GOAL]
case refine'_2.mk.mk.single.up.left.pair.up.left.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map
        (Pairwise.Hom.left { down := WalkingPair.left } { down := down✝ }).op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.left } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map (Pairwise.Hom.left { down := WalkingPair.left } { down := down✝ }).op
[PROOFSTEP]
dsimp [Pairwise.diagram]
[GOAL]
case refine'_2.mk.mk.single.up.left.pair.up.left.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map
        (Pairwise.Hom.right { down := WalkingPair.left } { down := WalkingPair.left }).op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.left } { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map
        (Pairwise.Hom.right { down := WalkingPair.left } { down := WalkingPair.left }).op
[PROOFSTEP]
dsimp [Pairwise.diagram]
[GOAL]
case refine'_2.mk.mk.single.up.left.pair.up.right.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map
        (Pairwise.Hom.right { down := WalkingPair.right } { down := WalkingPair.left }).op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.right } { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.left } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map
        (Pairwise.Hom.right { down := WalkingPair.right } { down := WalkingPair.left }).op
[PROOFSTEP]
dsimp [Pairwise.diagram]
[GOAL]
case refine'_2.mk.mk.single.up.right.single.up.right.id_single
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map
        (Pairwise.Hom.id_single { down := WalkingPair.right }).op ≫
      Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map (Pairwise.Hom.id_single { down := WalkingPair.right }).op
[PROOFSTEP]
dsimp [Pairwise.diagram]
[GOAL]
case refine'_2.mk.mk.single.up.right.pair.up.left.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map
        (Pairwise.Hom.right { down := WalkingPair.left } { down := WalkingPair.right }).op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.left } { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map
        (Pairwise.Hom.right { down := WalkingPair.left } { down := WalkingPair.right }).op
[PROOFSTEP]
dsimp [Pairwise.diagram]
[GOAL]
case refine'_2.mk.mk.single.up.right.pair.up.right.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map
        (Pairwise.Hom.left { down := WalkingPair.right } { down := down✝ }).op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.right } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map (Pairwise.Hom.left { down := WalkingPair.right } { down := down✝ }).op
[PROOFSTEP]
dsimp [Pairwise.diagram]
[GOAL]
case refine'_2.mk.mk.single.up.right.pair.up.right.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map
        (Pairwise.Hom.right { down := WalkingPair.right } { down := WalkingPair.right }).op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.right } { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.single { down := WalkingPair.right } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map
        (Pairwise.Hom.right { down := WalkingPair.right } { down := WalkingPair.right }).op
[PROOFSTEP]
dsimp [Pairwise.diagram]
[GOAL]
case refine'_2.mk.mk.pair.up.left.up.pair.up.left.up.id_pair
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map
        (Pairwise.Hom.id_pair { down := WalkingPair.left } { down := down✝ }).op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.left } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.left } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map
        (Pairwise.Hom.id_pair { down := WalkingPair.left } { down := down✝ }).op
[PROOFSTEP]
dsimp [Pairwise.diagram]
[GOAL]
case refine'_2.mk.mk.pair.up.right.up.pair.up.right.up.id_pair
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ).obj s.pt).map
        (Pairwise.Hom.id_pair { down := WalkingPair.right } { down := down✝ }).op ≫
      Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.right } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) =
    (Opposite.casesOn { unop := Pairwise.pair { down := WalkingPair.right } { down := down✝ } } 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 ⊓ ι a_1 ≤ U)).op)
              (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ ι a_1 ≤ V)).op)) ≫
      ((Pairwise.diagram ι).op ⋙ presheaf F).map
        (Pairwise.Hom.id_pair { down := WalkingPair.right } { down := down✝ }).op
[PROOFSTEP]
dsimp [Pairwise.diagram]
[GOAL]
case refine'_2.mk.mk.single.up.left.single.up.left.id_single
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ 𝟙 s.pt ≫ PullbackCone.fst s = PullbackCone.fst s ≫ (presheaf F).map (𝟙 (op U))
[PROOFSTEP]
simp only [Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]
[GOAL]
case refine'_2.mk.mk.single.up.left.pair.up.left.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
⊢ 𝟙 s.pt ≫ PullbackCone.fst s ≫ F.val.map (homOfLE (_ : U ⊓ WalkingPair.rec U V down✝ ≤ U)).op =
    PullbackCone.fst s ≫
      (presheaf F).map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.left }.down ⊓ WalkingPair.rec U V { down := down✝ }.down ≤
                WalkingPair.rec U V { down := WalkingPair.left }.down)).op
[PROOFSTEP]
simp only [Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]
[GOAL]
case refine'_2.mk.mk.single.up.left.pair.up.left.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ 𝟙 s.pt ≫ PullbackCone.fst s ≫ F.val.map (homOfLE (_ : U ⊓ U ≤ U)).op =
    PullbackCone.fst s ≫
      (presheaf F).map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.left }.down ⊓
                  WalkingPair.rec U V { down := WalkingPair.left }.down ≤
                WalkingPair.rec U V { down := WalkingPair.left }.down)).op
[PROOFSTEP]
simp only [Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]
[GOAL]
case refine'_2.mk.mk.single.up.left.pair.up.right.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ 𝟙 s.pt ≫ PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ U ≤ V)).op =
    PullbackCone.fst s ≫
      (presheaf F).map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.right }.down ⊓
                  WalkingPair.rec U V { down := WalkingPair.left }.down ≤
                WalkingPair.rec U V { down := WalkingPair.left }.down)).op
[PROOFSTEP]
simp only [Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]
[GOAL]
case refine'_2.mk.mk.single.up.right.single.up.right.id_single
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ 𝟙 s.pt ≫ PullbackCone.snd s = PullbackCone.snd s ≫ (presheaf F).map (𝟙 (op V))
[PROOFSTEP]
simp only [Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]
[GOAL]
case refine'_2.mk.mk.single.up.right.pair.up.left.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ 𝟙 s.pt ≫ PullbackCone.fst s ≫ F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op =
    PullbackCone.snd s ≫
      (presheaf F).map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.left }.down ⊓
                  WalkingPair.rec U V { down := WalkingPair.right }.down ≤
                WalkingPair.rec U V { down := WalkingPair.right }.down)).op
[PROOFSTEP]
simp only [Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]
[GOAL]
case refine'_2.mk.mk.single.up.right.pair.up.right.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
⊢ 𝟙 s.pt ≫ PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ WalkingPair.rec U V down✝ ≤ V)).op =
    PullbackCone.snd s ≫
      (presheaf F).map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.right }.down ⊓ WalkingPair.rec U V { down := down✝ }.down ≤
                WalkingPair.rec U V { down := WalkingPair.right }.down)).op
[PROOFSTEP]
simp only [Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]
[GOAL]
case refine'_2.mk.mk.single.up.right.pair.up.right.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ 𝟙 s.pt ≫ PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ V ≤ V)).op =
    PullbackCone.snd s ≫
      (presheaf F).map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.right }.down ⊓
                  WalkingPair.rec U V { down := WalkingPair.right }.down ≤
                WalkingPair.rec U V { down := WalkingPair.right }.down)).op
[PROOFSTEP]
simp only [Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]
[GOAL]
case refine'_2.mk.mk.pair.up.left.up.pair.up.left.up.id_pair
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
⊢ 𝟙 s.pt ≫ PullbackCone.fst s ≫ F.val.map (homOfLE (_ : U ⊓ WalkingPair.rec U V down✝ ≤ U)).op =
    (PullbackCone.fst s ≫ F.val.map (homOfLE (_ : U ⊓ WalkingPair.rec U V down✝ ≤ U)).op) ≫
      (presheaf F).map (𝟙 (op (U ⊓ WalkingPair.rec U V down✝)))
[PROOFSTEP]
simp only [Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]
[GOAL]
case refine'_2.mk.mk.pair.up.right.up.pair.up.right.up.id_pair
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
⊢ 𝟙 s.pt ≫ PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ WalkingPair.rec U V down✝ ≤ V)).op =
    (PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ WalkingPair.rec U V down✝ ≤ V)).op) ≫
      (presheaf F).map (𝟙 (op (V ⊓ WalkingPair.rec U V down✝)))
[PROOFSTEP]
simp only [Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]
[GOAL]
case refine'_2.mk.mk.single.up.left.pair.up.right.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ PullbackCone.snd s ≫ F.val.map (homOfLE (_ : V ⊓ U ≤ V)).op =
    PullbackCone.fst s ≫
      (presheaf F).map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.right }.down ⊓
                  WalkingPair.rec U V { down := WalkingPair.left }.down ≤
                WalkingPair.rec U V { down := WalkingPair.left }.down)).op
[PROOFSTEP]
rw [← cancel_mono (F.1.map (eqToHom <| inf_comm : U ⊓ V ⟶ _).op), Category.assoc, Category.assoc, ← F.1.map_comp, ←
  F.1.map_comp]
[GOAL]
case refine'_2.mk.mk.single.up.left.pair.up.right.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X := fun j => WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ PullbackCone.snd s ≫ F.val.map ((homOfLE (_ : V ⊓ U ≤ V)).op ≫ (eqToHom (_ : U ⊓ V = V ⊓ U)).op) =
    PullbackCone.fst s ≫
      F.val.map
        ((homOfLE
              (_ :
                WalkingPair.rec U V { down := WalkingPair.right }.down ⊓
                    WalkingPair.rec U V { down := WalkingPair.left }.down ≤
                  WalkingPair.rec U V { down := WalkingPair.left }.down)).op ≫
          (eqToHom (_ : U ⊓ V = V ⊓ U)).op)
[PROOFSTEP]
exact s.condition.symm
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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
[PROOFSTEP]
erw [Category.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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
[PROOFSTEP]
simp_rw [← F.1.map_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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
[PROOFSTEP]
exact
  (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 _).some.fac _ <|
    op <| Pairwise.single <| ULift.up WalkingPair.left
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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 (_ : V ≤ U ⊔ V)).op = PullbackCone.snd s
[PROOFSTEP]
erw [Category.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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 (_ : V ≤ U ⊔ V)).op =
    PullbackCone.snd s
[PROOFSTEP]
simp_rw [← F.1.map_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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 (_ : V ≤ U ⊔ V)).op) =
    PullbackCone.snd s
[PROOFSTEP]
exact
  (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 _).some.fac _ <|
    op <| Pairwise.single <| ULift.up WalkingPair.right
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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 (interUnionPullbackCone F U V)
[PROOFSTEP]
let ι : ULift.{w} WalkingPair → Opens X := fun ⟨j⟩ => WalkingPair.casesOn j U V
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
⊢ IsLimit (interUnionPullbackCone F U V)
[PROOFSTEP]
have hι : U ⊔ V = iSup ι := by
  ext
  rw [Opens.coe_iSup, Set.mem_iUnion]
  constructor
  · rintro (h | h)
    exacts [⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩]
  · rintro ⟨⟨_ | _⟩, h⟩
    exacts [Or.inl h, Or.inr h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
⊢ U ⊔ V = iSup ι
[PROOFSTEP]
ext
[GOAL]
case h.h
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) ↔ x✝ ∈ ↑(iSup ι)
[PROOFSTEP]
rw [Opens.coe_iSup, Set.mem_iUnion]
[GOAL]
case h.h
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) ↔
    ∃ i,
      x✝ ∈
        ↑(match i with
          | { down := j } => WalkingPair.casesOn j U V)
[PROOFSTEP]
constructor
[GOAL]
case h.h.mp
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) →
    ∃ i,
      x✝ ∈
        ↑(match i with
          | { down := j } => WalkingPair.casesOn j U V)
[PROOFSTEP]
rintro (h | h)
[GOAL]
case h.h.mp.inl
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
x✝ : ↑X
h : x✝ ∈ ↑U
⊢ ∃ i,
    x✝ ∈
      ↑(match i with
        | { down := j } => WalkingPair.casesOn j U V)
case h.h.mp.inr
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
x✝ : ↑X
h : x✝ ∈ ↑V
⊢ ∃ i,
    x✝ ∈
      ↑(match i with
        | { down := j } => WalkingPair.casesOn j U V)
[PROOFSTEP]
exacts [⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩]
[GOAL]
case h.h.mpr
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
x✝ : ↑X
⊢ (∃ i,
      x✝ ∈
        ↑(match i with
          | { down := j } => WalkingPair.casesOn j U V)) →
    x✝ ∈ ↑(U ⊔ V)
[PROOFSTEP]
rintro ⟨⟨_ | _⟩, h⟩
[GOAL]
case h.h.mpr.intro.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
x✝ : ↑X
h :
  x✝ ∈
    ↑(match { down := WalkingPair.left } with
      | { down := j } => WalkingPair.casesOn j U V)
⊢ x✝ ∈ ↑(U ⊔ V)
case h.h.mpr.intro.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
x✝ : ↑X
h :
  x✝ ∈
    ↑(match { down := WalkingPair.right } with
      | { down := j } => WalkingPair.casesOn j U V)
⊢ x✝ ∈ ↑(U ⊔ V)
[PROOFSTEP]
exacts [Or.inl h, Or.inr h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
⊢ IsLimit (interUnionPullbackCone F U V)
[PROOFSTEP]
apply PullbackCone.isLimitAux'
[GOAL]
case create
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
⊢ (s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)) →
    { l //
      l ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s ∧
        l ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s ∧
          ∀ {m : s.pt ⟶ (interUnionPullbackCone F U V).pt},
            m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s →
              m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s → m = l }
[PROOFSTEP]
intro s
[GOAL]
case create
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
⊢ { l //
    l ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s ∧
      l ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s ∧
        ∀ {m : s.pt ⟶ (interUnionPullbackCone F U V).pt},
          m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s →
            m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s → m = l }
[PROOFSTEP]
use interUnionPullbackConeLift F U V s
[GOAL]
case property
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
⊢ interUnionPullbackConeLift F U V s ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s ∧
    interUnionPullbackConeLift F U V s ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s ∧
      ∀ {m : s.pt ⟶ (interUnionPullbackCone F U V).pt},
        m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s →
          m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s →
            m = interUnionPullbackConeLift F U V s
[PROOFSTEP]
refine' ⟨_, _, _⟩
[GOAL]
case property.refine'_1
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
⊢ interUnionPullbackConeLift F U V s ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
[PROOFSTEP]
apply interUnionPullbackConeLift_left
[GOAL]
case property.refine'_2
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
⊢ interUnionPullbackConeLift F U V s ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
[PROOFSTEP]
apply interUnionPullbackConeLift_right
[GOAL]
case property.refine'_3
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
⊢ ∀ {m : s.pt ⟶ (interUnionPullbackCone F U V).pt},
    m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s →
      m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s → m = interUnionPullbackConeLift F U V s
[PROOFSTEP]
intro m h₁ h₂
[GOAL]
case property.refine'_3
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
⊢ m = interUnionPullbackConeLift F U V s
[PROOFSTEP]
rw [← cancel_mono (F.1.map (eqToHom hι.symm).op)]
[GOAL]
case property.refine'_3
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
⊢ m ≫ F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op =
    interUnionPullbackConeLift F U V s ≫ F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op
[PROOFSTEP]
apply (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 ι).some.hom_ext
[GOAL]
case property.refine'_3
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
⊢ ∀ (j : (CategoryTheory.Pairwise (ULift WalkingPair))ᵒᵖ),
    (m ≫ F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op) ≫
        NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π j =
      (interUnionPullbackConeLift F U V s ≫ F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op) ≫
        NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π j
[PROOFSTEP]
rintro ((_ | _) | (_ | _))
[GOAL]
case property.refine'_3.mk.single.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
⊢ (m ≫ F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op) ≫
      NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
        { unop := Pairwise.single { down := WalkingPair.left } } =
    (interUnionPullbackConeLift F U V s ≫ F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op) ≫
      NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
        { unop := Pairwise.single { down := WalkingPair.left } }
[PROOFSTEP]
rw [Category.assoc, Category.assoc]
[GOAL]
case property.refine'_3.mk.single.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
⊢ (m ≫ F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op) ≫
      NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
        { unop := Pairwise.single { down := WalkingPair.right } } =
    (interUnionPullbackConeLift F U V s ≫ F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op) ≫
      NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
        { unop := Pairwise.single { down := WalkingPair.right } }
[PROOFSTEP]
rw [Category.assoc, Category.assoc]
[GOAL]
case property.refine'_3.mk.pair.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ (m ≫ F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op) ≫
      NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
        { unop := Pairwise.pair { down := WalkingPair.left } a✝ } =
    (interUnionPullbackConeLift F U V s ≫ F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op) ≫
      NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
        { unop := Pairwise.pair { down := WalkingPair.left } a✝ }
[PROOFSTEP]
rw [Category.assoc, Category.assoc]
[GOAL]
case property.refine'_3.mk.pair.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ (m ≫ F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op) ≫
      NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
        { unop := Pairwise.pair { down := WalkingPair.right } a✝ } =
    (interUnionPullbackConeLift F U V s ≫ F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op) ≫
      NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
        { unop := Pairwise.pair { down := WalkingPair.right } a✝ }
[PROOFSTEP]
rw [Category.assoc, Category.assoc]
[GOAL]
case property.refine'_3.mk.single.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
⊢ m ≫
      F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op ≫
        NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
          { unop := Pairwise.single { down := WalkingPair.left } } =
    interUnionPullbackConeLift F U V s ≫
      F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op ≫
        NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
          { unop := Pairwise.single { down := WalkingPair.left } }
[PROOFSTEP]
erw [← F.1.map_comp]
[GOAL]
case property.refine'_3.mk.single.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
⊢ m ≫
      F.val.map
        ((eqToHom (_ : iSup ι = U ⊔ V)).op ≫
          NatTrans.app (Cocone.op (Pairwise.cocone ι)).π { unop := Pairwise.single { down := WalkingPair.left } }) =
    interUnionPullbackConeLift F U V s ≫
      F.val.map
        ((eqToHom (_ : iSup ι = U ⊔ V)).op ≫
          NatTrans.app (Cocone.op (Pairwise.cocone ι)).π { unop := Pairwise.single { down := WalkingPair.left } })
[PROOFSTEP]
convert h₁
[GOAL]
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
e_1✝ :
  (s.pt ⟶ ((Pairwise.diagram ι).op ⋙ presheaf F).obj { unop := Pairwise.single { down := WalkingPair.left } }) =
    (s.pt ⟶ F.val.obj (op U))
⊢ interUnionPullbackConeLift F U V s ≫
      F.val.map
        ((eqToHom (_ : iSup ι = U ⊔ V)).op ≫
          NatTrans.app (Cocone.op (Pairwise.cocone ι)).π { unop := Pairwise.single { down := WalkingPair.left } }) =
    PullbackCone.fst s
[PROOFSTEP]
apply interUnionPullbackConeLift_left
[GOAL]
case property.refine'_3.mk.single.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
⊢ m ≫
      F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op ≫
        NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
          { unop := Pairwise.single { down := WalkingPair.right } } =
    interUnionPullbackConeLift F U V s ≫
      F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op ≫
        NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
          { unop := Pairwise.single { down := WalkingPair.right } }
[PROOFSTEP]
erw [← F.1.map_comp]
[GOAL]
case property.refine'_3.mk.single.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
⊢ m ≫
      F.val.map
        ((eqToHom (_ : iSup ι = U ⊔ V)).op ≫
          NatTrans.app (Cocone.op (Pairwise.cocone ι)).π { unop := Pairwise.single { down := WalkingPair.right } }) =
    interUnionPullbackConeLift F U V s ≫
      F.val.map
        ((eqToHom (_ : iSup ι = U ⊔ V)).op ≫
          NatTrans.app (Cocone.op (Pairwise.cocone ι)).π { unop := Pairwise.single { down := WalkingPair.right } })
[PROOFSTEP]
convert h₂
[GOAL]
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
e_1✝ :
  (s.pt ⟶ ((Pairwise.diagram ι).op ⋙ presheaf F).obj { unop := Pairwise.single { down := WalkingPair.right } }) =
    (s.pt ⟶ F.val.obj (op V))
⊢ interUnionPullbackConeLift F U V s ≫
      F.val.map
        ((eqToHom (_ : iSup ι = U ⊔ V)).op ≫
          NatTrans.app (Cocone.op (Pairwise.cocone ι)).π { unop := Pairwise.single { down := WalkingPair.right } }) =
    PullbackCone.snd s
[PROOFSTEP]
apply interUnionPullbackConeLift_right
[GOAL]
case property.refine'_3.mk.pair.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ m ≫
      F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op ≫
        NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
          { unop := Pairwise.pair { down := WalkingPair.left } a✝ } =
    interUnionPullbackConeLift F U V s ≫
      F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op ≫
        NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
          { unop := Pairwise.pair { down := WalkingPair.left } a✝ }
case property.refine'_3.mk.pair.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ m ≫
      F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op ≫
        NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
          { unop := Pairwise.pair { down := WalkingPair.right } a✝ } =
    interUnionPullbackConeLift F U V s ≫
      F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op ≫
        NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
          { unop := Pairwise.pair { down := WalkingPair.right } a✝ }
[PROOFSTEP]
all_goals
  dsimp only [Functor.op, Pairwise.cocone_ι_app, Functor.mapCone_π_app, Cocone.op, Pairwise.coconeιApp, unop_op,
    op_comp, NatTrans.op]
  simp_rw [F.1.map_comp, ← Category.assoc]
  congr 1
  simp_rw [Category.assoc, ← F.1.map_comp]
[GOAL]
case property.refine'_3.mk.pair.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ m ≫
      F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op ≫
        NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
          { unop := Pairwise.pair { down := WalkingPair.left } a✝ } =
    interUnionPullbackConeLift F U V s ≫
      F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op ≫
        NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
          { unop := Pairwise.pair { down := WalkingPair.left } a✝ }
[PROOFSTEP]
dsimp only [Functor.op, Pairwise.cocone_ι_app, Functor.mapCone_π_app, Cocone.op, Pairwise.coconeιApp, unop_op, op_comp,
  NatTrans.op]
[GOAL]
case property.refine'_3.mk.pair.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ m ≫
      F.val.map (eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op ≫
        (presheaf F).map
          ((homOfLE
                (_ :
                  WalkingPair.rec U V { down := WalkingPair.left }.down ≤
                    ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op ≫
            (homOfLE
                (_ :
                  WalkingPair.rec U V { down := WalkingPair.left }.down ⊓ WalkingPair.rec U V a✝.down ≤
                    WalkingPair.rec U V { down := WalkingPair.left }.down)).op) =
    interUnionPullbackConeLift F U V s ≫
      F.val.map (eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op ≫
        (presheaf F).map
          ((homOfLE
                (_ :
                  WalkingPair.rec U V { down := WalkingPair.left }.down ≤
                    ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op ≫
            (homOfLE
                (_ :
                  WalkingPair.rec U V { down := WalkingPair.left }.down ⊓ WalkingPair.rec U V a✝.down ≤
                    WalkingPair.rec U V { down := WalkingPair.left }.down)).op)
[PROOFSTEP]
simp_rw [F.1.map_comp, ← Category.assoc]
[GOAL]
case property.refine'_3.mk.pair.up.left
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ ((m ≫ F.val.map (eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op) ≫
        F.val.map
          (homOfLE
              (_ :
                WalkingPair.rec U V { down := WalkingPair.left }.down ≤
                  ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op) ≫
      F.val.map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.left }.down ⊓ WalkingPair.rec U V a✝.down ≤
                WalkingPair.rec U V { down := WalkingPair.left }.down)).op =
    ((interUnionPullbackConeLift F U V s ≫
          F.val.map (eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op) ≫
        F.val.map
          (homOfLE
              (_ :
                WalkingPair.rec U V { down := WalkingPair.left }.down ≤
                  ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op) ≫
      F.val.map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.left }.down ⊓ WalkingPair.rec U V a✝.down ≤
                WalkingPair.rec U V { down := WalkingPair.left }.down)).op
[PROOFSTEP]
congr 1
[GOAL]
case property.refine'_3.mk.pair.up.left.e_a
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ (m ≫ F.val.map (eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op) ≫
      F.val.map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.left }.down ≤
                ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op =
    (interUnionPullbackConeLift F U V s ≫
        F.val.map (eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op) ≫
      F.val.map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.left }.down ≤
                ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op
[PROOFSTEP]
simp_rw [Category.assoc, ← F.1.map_comp]
[GOAL]
case property.refine'_3.mk.pair.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ m ≫
      F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op ≫
        NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
          { unop := Pairwise.pair { down := WalkingPair.right } a✝ } =
    interUnionPullbackConeLift F U V s ≫
      F.val.map (eqToHom (_ : iSup ι = U ⊔ V)).op ≫
        NatTrans.app ((presheaf F).mapCone (Cocone.op (Pairwise.cocone ι))).π
          { unop := Pairwise.pair { down := WalkingPair.right } a✝ }
[PROOFSTEP]
dsimp only [Functor.op, Pairwise.cocone_ι_app, Functor.mapCone_π_app, Cocone.op, Pairwise.coconeιApp, unop_op, op_comp,
  NatTrans.op]
[GOAL]
case property.refine'_3.mk.pair.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ m ≫
      F.val.map (eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op ≫
        (presheaf F).map
          ((homOfLE
                (_ :
                  WalkingPair.rec U V { down := WalkingPair.right }.down ≤
                    ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op ≫
            (homOfLE
                (_ :
                  WalkingPair.rec U V { down := WalkingPair.right }.down ⊓ WalkingPair.rec U V a✝.down ≤
                    WalkingPair.rec U V { down := WalkingPair.right }.down)).op) =
    interUnionPullbackConeLift F U V s ≫
      F.val.map (eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op ≫
        (presheaf F).map
          ((homOfLE
                (_ :
                  WalkingPair.rec U V { down := WalkingPair.right }.down ≤
                    ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op ≫
            (homOfLE
                (_ :
                  WalkingPair.rec U V { down := WalkingPair.right }.down ⊓ WalkingPair.rec U V a✝.down ≤
                    WalkingPair.rec U V { down := WalkingPair.right }.down)).op)
[PROOFSTEP]
simp_rw [F.1.map_comp, ← Category.assoc]
[GOAL]
case property.refine'_3.mk.pair.up.right
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ ((m ≫ F.val.map (eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op) ≫
        F.val.map
          (homOfLE
              (_ :
                WalkingPair.rec U V { down := WalkingPair.right }.down ≤
                  ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op) ≫
      F.val.map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.right }.down ⊓ WalkingPair.rec U V a✝.down ≤
                WalkingPair.rec U V { down := WalkingPair.right }.down)).op =
    ((interUnionPullbackConeLift F U V s ≫
          F.val.map (eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op) ≫
        F.val.map
          (homOfLE
              (_ :
                WalkingPair.rec U V { down := WalkingPair.right }.down ≤
                  ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op) ≫
      F.val.map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.right }.down ⊓ WalkingPair.rec U V a✝.down ≤
                WalkingPair.rec U V { down := WalkingPair.right }.down)).op
[PROOFSTEP]
congr 1
[GOAL]
case property.refine'_3.mk.pair.up.right.e_a
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ (m ≫ F.val.map (eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op) ≫
      F.val.map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.right }.down ≤
                ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op =
    (interUnionPullbackConeLift F U V s ≫
        F.val.map (eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op) ≫
      F.val.map
        (homOfLE
            (_ :
              WalkingPair.rec U V { down := WalkingPair.right }.down ≤
                ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op
[PROOFSTEP]
simp_rw [Category.assoc, ← F.1.map_comp]
[GOAL]
case property.refine'_3.mk.pair.up.left.e_a
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ m ≫
      F.val.map
        ((eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op ≫
          (homOfLE
              (_ :
                WalkingPair.rec U V { down := WalkingPair.left }.down ≤
                  ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op) =
    interUnionPullbackConeLift F U V s ≫
      F.val.map
        ((eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op ≫
          (homOfLE
              (_ :
                WalkingPair.rec U V { down := WalkingPair.left }.down ≤
                  ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op)
[PROOFSTEP]
convert h₁
[GOAL]
case h.e'_3
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ interUnionPullbackConeLift F U V s ≫
      F.val.map
        ((eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op ≫
          (homOfLE
              (_ :
                WalkingPair.rec U V { down := WalkingPair.left }.down ≤
                  ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op) =
    PullbackCone.fst s
[PROOFSTEP]
apply interUnionPullbackConeLift_left
[GOAL]
case property.refine'_3.mk.pair.up.right.e_a
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ m ≫
      F.val.map
        ((eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op ≫
          (homOfLE
              (_ :
                WalkingPair.rec U V { down := WalkingPair.right }.down ≤
                  ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op) =
    interUnionPullbackConeLift F U V s ≫
      F.val.map
        ((eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op ≫
          (homOfLE
              (_ :
                WalkingPair.rec U V { down := WalkingPair.right }.down ≤
                  ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op)
[PROOFSTEP]
convert h₂
[GOAL]
case h.e'_3
C : Type u
inst✝ : Category.{v, u} 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)
ι : ULift WalkingPair → Opens ↑X :=
  fun x =>
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.val.map (homOfLE (_ : U ⊓ V ≤ U)).op) (F.val.map (homOfLE (_ : U ⊓ V ≤ V)).op)
m : s.pt ⟶ (interUnionPullbackCone F U V).pt
h₁ : m ≫ PullbackCone.fst (interUnionPullbackCone F U V) = PullbackCone.fst s
h₂ : m ≫ PullbackCone.snd (interUnionPullbackCone F U V) = PullbackCone.snd s
a✝ : ULift WalkingPair
⊢ interUnionPullbackConeLift F U V s ≫
      F.val.map
        ((eqToHom (_ : ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down = U ⊔ V)).op ≫
          (homOfLE
              (_ :
                WalkingPair.rec U V { down := WalkingPair.right }.down ≤
                  ⨆ (x : ULift WalkingPair), WalkingPair.rec U V x.down)).op) =
    PullbackCone.snd s
[PROOFSTEP]
apply interUnionPullbackConeLift_right
