C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
⊢ IsIso (stalkPushforward C f F x)
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
⊢ IsIso (stalkPushforward C f F x)
haveI := Functor.initial_of_adjunction (hf.isOpenMap.adjunctionNhds x)
case h.e'_5.h
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
⊢ stalkPushforward C f F x =
    ((Functor.Final.colimitIso (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x))
            (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)).symm ≪≫
        colim.mapIso ?convert_2).hom

case convert_2
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
⊢ Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x) ⋙
      Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F ≅
    ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
⊢ IsIso (stalkPushforward C f F x)
convert IsIso.of_iso
    ((Functor.Final.colimitIso (hf.isOpenMap.functorNhds x).op
            ((OpenNhds.inclusion (f x)).op ⋙ f _* F) :
          _).symm ≪≫
      colim.mapIso _)
case convert_2
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
⊢ Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x) ⋙
      Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F ≅
    ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F

case h.e'_5.h
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
⊢ stalkPushforward C f F x =
    ((Functor.Final.colimitIso (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x))
            (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)).symm ≪≫
        colim.mapIso ?convert_2).hom
case h.e'_5.h
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
⊢ stalkPushforward C f F x =
    ((Functor.Final.colimitIso (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x))
            (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)).symm ≪≫
        colim.mapIso ?convert_2).hom

case convert_2
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
⊢ Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x) ⋙
      Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F ≅
    ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F
swap
case convert_2.app
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
⊢ (X_1 : (OpenNhds x)ᵒᵖ) →
    (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x) ⋙
            Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F).obj
        X_1 ≅
      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F).obj X_1

case convert_2.naturality
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
⊢ autoParam
    (∀ {X_1 Y_1 : (OpenNhds x)ᵒᵖ} (f_1 : X_1 ⟶ Y_1),
      (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x) ⋙
                Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F).map
            f_1 ≫
          (?convert_2.app Y_1).hom =
        (?convert_2.app X_1).hom ≫
          (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F).map f_1)
    _auto✝
case convert_2
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
⊢ Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x) ⋙
      Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F ≅
    ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F
fapply NatIso.ofComponents
case convert_2.app
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
U : (OpenNhds x)ᵒᵖ
⊢ (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x) ⋙
          Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F).obj
      U ≅
    (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F).obj U
case convert_2.app
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
⊢ (X_1 : (OpenNhds x)ᵒᵖ) →
    (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x) ⋙
            Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F).obj
        X_1 ≅
      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F).obj X_1
intro U
case convert_2.app
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
U : (OpenNhds x)ᵒᵖ
⊢ (Functor.op (Opens.map f)).obj
      ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
        ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
    (Functor.op (OpenNhds.inclusion x)).obj U
case convert_2.app
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
U : (OpenNhds x)ᵒᵖ
⊢ (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x) ⋙
          Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F).obj
      U ≅
    (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F).obj U
refine' F.mapIso (eqToIso _)
case convert_2.app
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
U : (OpenNhds x)ᵒᵖ
⊢ ((Opens.map f).obj
        ((OpenNhds.inclusion ((forget TopCat).map f x)).obj
              ((IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x).obj U.unop).op.unop).op.unop).op =
    ((OpenNhds.inclusion x).obj U.unop).op
case convert_2.app
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
U : (OpenNhds x)ᵒᵖ
⊢ (Functor.op (Opens.map f)).obj
      ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
        ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
    (Functor.op (OpenNhds.inclusion x)).obj U
dsimp only [Functor.op]
no goals
case convert_2.app
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
U : (OpenNhds x)ᵒᵖ
⊢ ((Opens.map f).obj
        ((OpenNhds.inclusion ((forget TopCat).map f x)).obj
              ((IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x).obj U.unop).op.unop).op.unop).op =
    ((OpenNhds.inclusion x).obj U.unop).op
exact congr_arg op (Opens.ext <| Set.preimage_image_eq (unop U).1.1 hf.inj)
case convert_2.naturality
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
U V : (OpenNhds x)ᵒᵖ
i : U ⟶ V
⊢ (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x) ⋙
            Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F).map
        i ≫
      (F.mapIso
          (eqToIso
            (_ :
              (Functor.op (Opens.map f)).obj
                  ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                    ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj V)) =
                (Functor.op (OpenNhds.inclusion x)).obj V))).hom =
    (F.mapIso
          (eqToIso
            (_ :
              (Functor.op (Opens.map f)).obj
                  ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                    ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                (Functor.op (OpenNhds.inclusion x)).obj U))).hom ≫
      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F).map i
case convert_2.naturality
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
⊢ autoParam
    (∀ {X_1 Y_1 : (OpenNhds x)ᵒᵖ} (f_1 : X_1 ⟶ Y_1),
      (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x) ⋙
                Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F).map
            f_1 ≫
          (F.mapIso
              (eqToIso
                (_ :
                  (Functor.op (Opens.map f)).obj
                      ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                        ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj Y_1)) =
                    (Functor.op (OpenNhds.inclusion x)).obj Y_1))).hom =
        (F.mapIso
              (eqToIso
                (_ :
                  (Functor.op (Opens.map f)).obj
                      ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                        ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj X_1)) =
                    (Functor.op (OpenNhds.inclusion x)).obj X_1))).hom ≫
          (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F).map f_1)
    _auto✝
intro U V i
case convert_2.naturality
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
U V : (OpenNhds x)ᵒᵖ
i : U ⟶ V
⊢ F.map
      ((Functor.op (Opens.map f)).map
          ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).map
            ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).map i)) ≫
        (eqToIso
            (_ :
              (Functor.op (Opens.map f)).obj
                  ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                    ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj V)) =
                (Functor.op (OpenNhds.inclusion x)).obj V)).hom) =
    F.map
      ((eqToIso
            (_ :
              (Functor.op (Opens.map f)).obj
                  ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                    ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                (Functor.op (OpenNhds.inclusion x)).obj U)).hom ≫
        (Functor.op (OpenNhds.inclusion x)).map i)
case convert_2.naturality
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
U V : (OpenNhds x)ᵒᵖ
i : U ⟶ V
⊢ (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x) ⋙
            Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F).map
        i ≫
      (F.mapIso
          (eqToIso
            (_ :
              (Functor.op (Opens.map f)).obj
                  ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                    ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj V)) =
                (Functor.op (OpenNhds.inclusion x)).obj V))).hom =
    (F.mapIso
          (eqToIso
            (_ :
              (Functor.op (Opens.map f)).obj
                  ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                    ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                (Functor.op (OpenNhds.inclusion x)).obj U))).hom ≫
      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F).map i
erw [← F.map_comp, ← F.map_comp]
no goals
case convert_2.naturality
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
U V : (OpenNhds x)ᵒᵖ
i : U ⟶ V
⊢ F.map
      ((Functor.op (Opens.map f)).map
          ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).map
            ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).map i)) ≫
        (eqToIso
            (_ :
              (Functor.op (Opens.map f)).obj
                  ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                    ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj V)) =
                (Functor.op (OpenNhds.inclusion x)).obj V)).hom) =
    F.map
      ((eqToIso
            (_ :
              (Functor.op (Opens.map f)).obj
                  ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                    ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                (Functor.op (OpenNhds.inclusion x)).obj U)).hom ≫
        (Functor.op (OpenNhds.inclusion x)).map i)
congr 1
case h.e'_5.h
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
⊢ stalkPushforward C f F x =
    ((Functor.Final.colimitIso (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x))
            (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)).symm ≪≫
        colim.mapIso
          (NatIso.ofComponents fun U =>
            F.mapIso
              (eqToIso
                (_ :
                  (Functor.op (Opens.map f)).obj
                      ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                        ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                    (Functor.op (OpenNhds.inclusion x)).obj U)))).hom
case h.e'_5.h
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
⊢ stalkPushforward C f F x =
    ((Functor.Final.colimitIso (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x))
            (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)).symm ≪≫
        colim.mapIso
          (NatIso.ofComponents fun U =>
            F.mapIso
              (eqToIso
                (_ :
                  (Functor.op (Opens.map f)).obj
                      ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                        ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                    (Functor.op (OpenNhds.inclusion x)).obj U)))).hom
change (_ : colimit _ ⟶  _) = (_ : colimit _ ⟶  _)
case h.e'_5.h.w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map f x))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)))).obj
          (f _* F))
        U ≫
      stalkPushforward C f F x =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map f x))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)))).obj
          (f _* F))
        U ≫
      ((Functor.Final.colimitIso (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x))
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)).symm ≪≫
          colim.mapIso
            (NatIso.ofComponents fun U =>
              F.mapIso
                (eqToIso
                  (_ :
                    (Functor.op (Opens.map f)).obj
                        ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                          ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                      (Functor.op (OpenNhds.inclusion x)).obj U)))).hom
case h.e'_5.h
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
⊢ stalkPushforward C f F x =
    ((Functor.Final.colimitIso (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x))
            (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)).symm ≪≫
        colim.mapIso
          (NatIso.ofComponents fun U =>
            F.mapIso
              (eqToIso
                (_ :
                  (Functor.op (Opens.map f)).obj
                      ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                        ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                    (Functor.op (OpenNhds.inclusion x)).obj U)))).hom
ext U
case h.e'_5.h.w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ (colimit.ι
          (((whiskeringLeft (OpenNhds ((forget TopCat).map f x))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj
                (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)))).obj
            (f _* F))
          U ≫
        stalkPushforward C f F x) ≫
      ((Functor.Final.colimitIso (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x))
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)).symm ≪≫
          colim.mapIso
            (NatIso.ofComponents fun U =>
              F.mapIso
                (eqToIso
                  (_ :
                    (Functor.op (Opens.map f)).obj
                        ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                          ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                      (Functor.op (OpenNhds.inclusion x)).obj U)))).inv =
    colimit.ι
      (((whiskeringLeft (OpenNhds ((forget TopCat).map f x))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj
            (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)))).obj
        (f _* F))
      U
case h.e'_5.h.w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map f x))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)))).obj
          (f _* F))
        U ≫
      stalkPushforward C f F x =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map f x))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)))).obj
          (f _* F))
        U ≫
      ((Functor.Final.colimitIso (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x))
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)).symm ≪≫
          colim.mapIso
            (NatIso.ofComponents fun U =>
              F.mapIso
                (eqToIso
                  (_ :
                    (Functor.op (Opens.map f)).obj
                        ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                          ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                      (Functor.op (OpenNhds.inclusion x)).obj U)))).hom
rw [← Iso.comp_inv_eq]
case h.e'_5.h.w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ ((whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f x).inv) F).app U ≫
        colimit.ι
            (Functor.op (OpenNhds.map f x) ⋙
              ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
            U ≫
          colimit.pre (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
            (Functor.op (OpenNhds.map f x))) ≫
      ((Functor.Final.colimitIso (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x))
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)).symm ≪≫
          colim.mapIso
            (NatIso.ofComponents fun U =>
              F.mapIso
                (eqToIso
                  (_ :
                    (Functor.op (Opens.map f)).obj
                        ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                          ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                      (Functor.op (OpenNhds.inclusion x)).obj U)))).inv =
    colimit.ι
      (((whiskeringLeft (OpenNhds ((forget TopCat).map f x))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj
            (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)))).obj
        (f _* F))
      U
case h.e'_5.h.w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ (colimit.ι
          (((whiskeringLeft (OpenNhds ((forget TopCat).map f x))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj
                (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)))).obj
            (f _* F))
          U ≫
        stalkPushforward C f F x) ≫
      ((Functor.Final.colimitIso (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x))
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)).symm ≪≫
          colim.mapIso
            (NatIso.ofComponents fun U =>
              F.mapIso
                (eqToIso
                  (_ :
                    (Functor.op (Opens.map f)).obj
                        ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                          ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                      (Functor.op (OpenNhds.inclusion x)).obj U)))).inv =
    colimit.ι
      (((whiskeringLeft (OpenNhds ((forget TopCat).map f x))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj
            (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)))).obj
        (f _* F))
      U
erw [colimit.ι_map_assoc]
case h.e'_5.h.w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f x).inv) F).app U ≫
      colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
          ((Functor.op (OpenNhds.map f x)).obj U) ≫
        ((Functor.Final.colimitIso (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x))
                (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)).symm ≪≫
            colim.mapIso
              (NatIso.ofComponents fun U =>
                F.mapIso
                  (eqToIso
                    (_ :
                      (Functor.op (Opens.map f)).obj
                          ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                            ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                        (Functor.op (OpenNhds.inclusion x)).obj U)))).inv =
    colimit.ι
      (((whiskeringLeft (OpenNhds ((forget TopCat).map f x))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj
            (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)))).obj
        (f _* F))
      U
case h.e'_5.h.w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ ((whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f x).inv) F).app U ≫
        colimit.ι
            (Functor.op (OpenNhds.map f x) ⋙
              ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
            U ≫
          colimit.pre (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
            (Functor.op (OpenNhds.map f x))) ≫
      ((Functor.Final.colimitIso (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x))
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)).symm ≪≫
          colim.mapIso
            (NatIso.ofComponents fun U =>
              F.mapIso
                (eqToIso
                  (_ :
                    (Functor.op (Opens.map f)).obj
                        ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                          ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                      (Functor.op (OpenNhds.inclusion x)).obj U)))).inv =
    colimit.ι
      (((whiskeringLeft (OpenNhds ((forget TopCat).map f x))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj
            (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)))).obj
        (f _* F))
      U
rw [colimit.ι_pre, Category.assoc]
case h.e'_5.h.w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ F.map
        ((NatTrans.op (OpenNhds.inclusionMapIso f x).inv).app U ≫
          (eqToIso
              (_ :
                (Functor.op (Opens.map f)).obj
                    ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                      ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj
                        ((Functor.op (OpenNhds.map f x)).obj U))) =
                  (Functor.op (OpenNhds.inclusion x)).obj ((Functor.op (OpenNhds.map f x)).obj U))).inv) ≫
      colimit.ι (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
        ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj
          ((Functor.op (OpenNhds.map f x)).obj U)) =
    colimit.ι
      (((whiskeringLeft (OpenNhds ((forget TopCat).map f x))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj
            (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)))).obj
        (f _* F))
      U
case h.e'_5.h.w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f x).inv) F).app U ≫
      colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
          ((Functor.op (OpenNhds.map f x)).obj U) ≫
        ((Functor.Final.colimitIso (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x))
                (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)).symm ≪≫
            colim.mapIso
              (NatIso.ofComponents fun U =>
                F.mapIso
                  (eqToIso
                    (_ :
                      (Functor.op (Opens.map f)).obj
                          ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                            ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj U)) =
                        (Functor.op (OpenNhds.inclusion x)).obj U)))).inv =
    colimit.ι
      (((whiskeringLeft (OpenNhds ((forget TopCat).map f x))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj
            (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)))).obj
        (f _* F))
      U
erw [colimit.ι_map_assoc, colimit.ι_pre, ← F.map_comp_assoc]
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ U ⟶
    (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj
      ((Functor.op (OpenNhds.map f x)).obj U)
case h.e'_5.h.w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ F.map
        ((NatTrans.op (OpenNhds.inclusionMapIso f x).inv).app U ≫
          (eqToIso
              (_ :
                (Functor.op (Opens.map f)).obj
                    ((Functor.op (OpenNhds.inclusion ((forget TopCat).map f x))).obj
                      ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj
                        ((Functor.op (OpenNhds.map f x)).obj U))) =
                  (Functor.op (OpenNhds.inclusion x)).obj ((Functor.op (OpenNhds.map f x)).obj U))).inv) ≫
      colimit.ι (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
        ((Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj
          ((Functor.op (OpenNhds.map f x)).obj U)) =
    colimit.ι
      (((whiskeringLeft (OpenNhds ((forget TopCat).map f x))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj
            (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)))).obj
        (f _* F))
      U
apply colimit.w ((OpenNhds.inclusion (f x)).op ⋙ f _* F) _
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ U ⟶ ((IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x).obj ((OpenNhds.map f x).obj U.unop).op.unop).op
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ U ⟶
    (Functor.op (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)).obj
      ((Functor.op (OpenNhds.map f x)).obj U)
dsimp only [Functor.op]
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x).obj ((OpenNhds.map f x).obj U.unop).op.unop ≤ U.unop
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ U ⟶ ((IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x).obj ((OpenNhds.map f x).obj U.unop).op.unop).op
refine' ((homOfLE _).op : op (unop U) ⟶ _)
no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
hf : OpenEmbedding ((forget TopCat).map f)
F : Presheaf C X
x : ↑X
this : Functor.Initial (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x)
e_3✝ :
  stalk (f _* F) ((forget TopCat).map f x) =
    colimit (Functor.op (OpenNhds.inclusion ((forget TopCat).map f x)) ⋙ f _* F)
e_4✝ :
  stalk F x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion x))).obj F)
U : (OpenNhds ((forget TopCat).map f x))ᵒᵖ
⊢ (IsOpenMap.functorNhds (_ : IsOpenMap ((forget TopCat).map f)) x).obj ((OpenNhds.map f x).obj U.unop).op.unop ≤ U.unop
exact Set.image_preimage_subset _ _