[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
[PROOFSTEP]
have obj_eq :
  ∀ (j : Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
[GOAL]
case obj_eq
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
[PROOFSTEP]
rintro ⟨i⟩
[GOAL]
case obj_eq.single
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
i : ι
⊢ (Pairwise.diagram U ⋙ Opens.map f).obj (Pairwise.single i) =
    (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj (Pairwise.single i)
[PROOFSTEP]
rfl
[GOAL]
case obj_eq.pair
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
a✝¹ a✝ : ι
⊢ (Pairwise.diagram U ⋙ Opens.map f).obj (Pairwise.pair a✝¹ a✝) =
    (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj (Pairwise.pair a✝¹ a✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
[PROOFSTEP]
refine Functor.hext obj_eq ?_
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
⊢ ∀ (X_1 Y_1 : CategoryTheory.Pairwise ι) (f_1 : X_1 ⟶ Y_1),
    HEq ((Pairwise.diagram U ⋙ Opens.map f).map f_1) ((Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1)
[PROOFSTEP]
intro i j g
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
i j : CategoryTheory.Pairwise ι
g : i ⟶ j
⊢ HEq ((Pairwise.diagram U ⋙ Opens.map f).map g) ((Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map g)
[PROOFSTEP]
apply Subsingleton.helim
[GOAL]
case h₂
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
obj_eq :
  ∀ (j : CategoryTheory.Pairwise ι),
    (Pairwise.diagram U ⋙ Opens.map f).obj j = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j
i j : CategoryTheory.Pairwise ι
g : i ⟶ j
⊢ ((Pairwise.diagram U ⋙ Opens.map f).obj i ⟶ (Pairwise.diagram U ⋙ Opens.map f).obj j) =
    ((Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj i ⟶
      (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj j)
[PROOFSTEP]
rw [obj_eq, obj_eq]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
unfold Functor.mapCocone Cocones.functoriality
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    ((CategoryTheory.Functor.mk
          {
            obj := fun A =>
              { pt := (Opens.map f).obj A.pt, ι := NatTrans.mk fun j => (Opens.map f).map (NatTrans.app A.ι j) },
            map := fun {X_1 Y_1} f_1 => CoconeMorphism.mk ((Opens.map f).map f_1.Hom) }).obj
      (Pairwise.cocone U))
    (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq { pt := (Opens.map f).obj (iSup U), ι := NatTrans.mk fun j => (Opens.map f).map (Pairwise.coconeιApp U j) }
    (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
congr
[GOAL]
case e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case e_6.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_6.h.e_a
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_7
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq (fun j => (Opens.map f).map (Pairwise.coconeιApp U j)) (Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U))
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
iterate 2 rw [map_diagram]; rw [Opens.map_iSup]
[GOAL]
case e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case e_6.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_6.h.e_a
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_7
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq (fun j => (Opens.map f).map (Pairwise.coconeιApp U j)) (Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U))
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
rw [map_diagram]
[GOAL]
case e_6.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_6.h.e_a
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_7
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq (fun j => (Opens.map f).map (Pairwise.coconeιApp U j)) (Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U))
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
rw [Opens.map_iSup]
[GOAL]
case e_7.e_5.h
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ Pairwise.diagram U ⋙ Opens.map f = Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_6.h.e_a
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_7
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq (fun j => (Opens.map f).map (Pairwise.coconeιApp U j)) (Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U))
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
rw [map_diagram]
[GOAL]
case e_7.e_6.h.e_a
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ (Opens.map f).obj (iSup U) = iSup ((Opens.map f).toPrefunctor.obj ∘ U)
case e_7.e_7
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq (fun j => (Opens.map f).map (Pairwise.coconeιApp U j)) (Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U))
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
rw [Opens.map_iSup]
[GOAL]
case e_7.e_7
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq (fun j => (Opens.map f).map (Pairwise.coconeιApp U j)) (Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U))
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
apply Subsingleton.helim
[GOAL]
case e_7.e_7.h₂
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ ((X_1 : CategoryTheory.Pairwise ι) →
      (Pairwise.diagram U ⋙ Opens.map f).obj X_1 ⟶
        ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (iSup U))).obj X_1) =
    ((X_1 : CategoryTheory.Pairwise ι) →
      (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).obj X_1 ⟶
        ((Functor.const (CategoryTheory.Pairwise ι)).obj (iSup ((Opens.map f).toPrefunctor.obj ∘ U))).obj X_1)
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
rw [map_diagram, Opens.map_iSup]
[GOAL]
case e_7.e_8
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
⊢ HEq
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram U ⋙ Opens.map f).map f_1 ≫
            (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) Y_1 =
          (fun j => (Opens.map f).map (NatTrans.app (Pairwise.cocone U).ι j)) X_1 ≫
            ((Functor.const (CategoryTheory.Pairwise ι)).obj ((Opens.map f).obj (Pairwise.cocone U).pt)).map f_1)
    (_ :
      ∀ ⦃X_1 Y_1 : CategoryTheory.Pairwise ι⦄ (f_1 : X_1 ⟶ Y_1),
        (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).map f_1 ≫
            Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) Y_1 =
          Pairwise.coconeιApp ((Opens.map f).toPrefunctor.obj ∘ U) X_1 ≫ 𝟙 (iSup ((Opens.map f).toPrefunctor.obj ∘ U)))
[PROOFSTEP]
apply proof_irrel_heq
[GOAL]
C : Type u
inst✝ : Category.{v, u} 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))))
[PROOFSTEP]
convert h ((Opens.map f).obj ∘ U) using 2
[GOAL]
case h.e'_1.h.e'_5
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
⊢ (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
case h.e'_1.h.e'_6
C : Type u
inst✝ : Category.{v, u} 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✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq ((f _* F).mapCone (Cocone.op (Pairwise.cocone U)))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
[PROOFSTEP]
rw [← map_diagram]
[GOAL]
case h.e'_1.h.e'_5
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι✝ : Type w
U✝ : ι✝ → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑Y
⊢ (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram U ⋙ Opens.map f).op ⋙ F
case h.e'_1.h.e'_6
C : Type u
inst✝ : Category.{v, u} 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✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq ((f _* F).mapCone (Cocone.op (Pairwise.cocone U)))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
[PROOFSTEP]
rfl
[GOAL]
case h.e'_1.h.e'_6
C : Type u
inst✝ : Category.{v, u} 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✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq ((f _* F).mapCone (Cocone.op (Pairwise.cocone U)))
    (F.mapCone (Cocone.op (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))))
[PROOFSTEP]
change HEq (Functor.mapCone F ((Opens.map f).mapCocone (Pairwise.cocone U)).op) _
[GOAL]
case h.e'_1.h.e'_6
C : Type u
inst✝ : Category.{v, u} 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✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ 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))))
[PROOFSTEP]
congr
[GOAL]
case h.e'_1.h.e'_6.e_8.h.e_F
C : Type u
inst✝ : Category.{v, u} 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✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ 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.{v, u} 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✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ 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.{v, u} 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✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
iterate 2 rw [map_diagram]
[GOAL]
case h.e'_1.h.e'_6.e_8.h.e_F
C : Type u
inst✝ : Category.{v, u} 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✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ 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.{v, u} 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✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ 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.{v, u} 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✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
rw [map_diagram]
[GOAL]
case h.e'_1.h.e'_6.e_9.e_5.h
C : Type u
inst✝ : Category.{v, u} 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✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ 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.{v, u} 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✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
rw [map_diagram]
[GOAL]
case h.e'_1.h.e'_6.e_9.e_6
C : Type u
inst✝ : Category.{v, u} 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✝ : (Pairwise.diagram U).op ⋙ f _* F = (Pairwise.diagram ((Opens.map f).toPrefunctor.obj ∘ U)).op ⋙ F
⊢ HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) (Pairwise.cocone ((Opens.map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
apply mapCocone
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
F : Presheaf C X
h : Presheaf.IsSheaf F
⊢ Presheaf.IsSheaf (f _* F)
[PROOFSTEP]
rw [isSheaf_iff_isSheafPairwiseIntersections] at h ⊢
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
F : Presheaf C X
h : IsSheafPairwiseIntersections F
⊢ IsSheafPairwiseIntersections (f _* F)
[PROOFSTEP]
exact SheafConditionPairwiseIntersections.pushforward_sheaf_of_sheaf f h
