case h.e'_1.h.e'_5
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
⊢ Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F

case h.e'_1.h.e'_6
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ HEq ((f _* F).mapCone (Cocone.op (Pairwise.cocone U)))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
⊢ Nonempty (IsLimit ((f _* F).mapCone (Cocone.op (Pairwise.cocone U))))
convert h ((Opens.map f).obj ∘ U) using 2
case h.e'_1.h.e'_5
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
⊢ Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram U ⋙ Opens.map f) ⋙ F

case h.e'_1.h.e'_6
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ HEq ((f _* F).mapCone (Cocone.op (Pairwise.cocone U)))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
case h.e'_1.h.e'_5
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
⊢ Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F

case h.e'_1.h.e'_6
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ HEq ((f _* F).mapCone (Cocone.op (Pairwise.cocone U)))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
rw [← map_diagram]
case h.e'_1.h.e'_6
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ HEq ((f _* F).mapCone (Cocone.op (Pairwise.cocone U)))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
case h.e'_1.h.e'_5
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
⊢ Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram U ⋙ Opens.map f) ⋙ F

case h.e'_1.h.e'_6
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ HEq ((f _* F).mapCone (Cocone.op (Pairwise.cocone U)))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
rfl
case h.e'_1.h.e'_6
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ HEq (F.mapCone (Cocone.op ((Opens.map f).mapCocone (Pairwise.cocone U))))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
case h.e'_1.h.e'_6
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ HEq ((f _* F).mapCone (Cocone.op (Pairwise.cocone U)))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
change HEq (Functor.mapCone F ((Opens.map f).mapCocone (Pairwise.cocone U)).op) _
case h.e'_1.h.e'_6.e_8.h.e_F
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)

case h.e'_1.h.e'_6.e_9.e_5.h
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)

case h.e'_1.h.e'_6.e_9.e_6
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
case h.e'_1.h.e'_6
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ HEq (F.mapCone (Cocone.op ((Opens.map f).mapCocone (Pairwise.cocone U))))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
congr
case h.e'_1.h.e'_6.e_9.e_6
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
case h.e'_1.h.e'_6.e_8.h.e_F
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)

case h.e'_1.h.e'_6.e_9.e_5.h
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)

case h.e'_1.h.e'_6.e_9.e_6
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
iterate 2 rw [map_diagram]
no goals
case h.e'_1.h.e'_6.e_9.e_6
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
apply mapCocone
case h.e'_1.h.e'_6.e_9.e_6
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
case h.e'_1.h.e'_6.e_9.e_5.h
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)

case h.e'_1.h.e'_6.e_9.e_6
C : Type u
inst✝ : Category C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
e_5✝ : Functor.op (Pairwise.diagram U) ⋙ f _* F = Functor.op (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)) ⋙ F
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
rw [map_diagram]