[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
U : Opens ↑↑Y
x : { x // x ∈ (Opens.map α.base).obj U }
⊢ germ Y.presheaf { val := ↑α.base ↑x, property := (_ : ↑x ∈ (Opens.map α.base).obj U) } ≫ stalkMap α ↑x =
    NatTrans.app α.c (op U) ≫ germ X.presheaf x
[PROOFSTEP]
rw [stalkMap, stalkFunctor_map_germ_assoc, stalkPushforward_germ]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
V : Opens ↑U
x : ↑U
hx : x ∈ V
⊢ germ X.presheaf { val := ↑f x, property := (_ : ↑f x ∈ (IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V) } ≫
      (restrictStalkIso X h x).inv =
    germ (restrict X h).presheaf { val := x, property := hx }
[PROOFSTEP]
rw [← restrictStalkIso_hom_eq_germ, Category.assoc, Iso.hom_inv_id, Category.comp_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
⊢ (restrictStalkIso X h x).inv = stalkMap (ofRestrict X h) x
[PROOFSTEP]
refine colimit.hom_ext fun V => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : (OpenNhds (↑f x))ᵒᵖ
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        V ≫
      (restrictStalkIso X h x).inv =
    colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        V ≫
      stalkMap (ofRestrict X h) x
[PROOFSTEP]
induction V with
| h V => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : (OpenNhds (↑f x))ᵒᵖ
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        V ≫
      (restrictStalkIso X h x).inv =
    colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        V ≫
      stalkMap (ofRestrict X h) x
[PROOFSTEP]
induction V with
| h V => ?_
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : OpenNhds (↑f x)
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        (op V) ≫
      (restrictStalkIso X h x).inv =
    colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        (op V) ≫
      stalkMap (ofRestrict X h) x
[PROOFSTEP]
let i : (h.isOpenMap.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE (Set.image_preimage_subset f _)
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : OpenNhds (↑f x)
i : (IsOpenMap.functorNhds (_ : IsOpenMap ↑f) x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
  homOfLE (_ : ↑f '' (↑f ⁻¹' V.obj.1) ⊆ V.obj.1)
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        (op V) ≫
      (restrictStalkIso X h x).inv =
    colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        (op V) ≫
      stalkMap (ofRestrict X h) x
[PROOFSTEP]
erw [Iso.comp_inv_eq, colimit.ι_map_assoc, colimit.ι_map_assoc, colimit.ι_pre]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : OpenNhds (↑f x)
i : (IsOpenMap.functorNhds (_ : IsOpenMap ↑f) x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
  homOfLE (_ : ↑f '' (↑f ⁻¹' V.obj.1) ⊆ V.obj.1)
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
      (op V) =
    (NatTrans.app
          (((whiskeringLeft (OpenNhds (↑(ofRestrict X h).base x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                (OpenNhds.inclusion (↑(ofRestrict X h).base x)).op).map
            (ofRestrict X h).c)
          (op V) ≫
        NatTrans.app
            (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (ofRestrict X h).base x).inv) (restrict X h).presheaf)
            (op V) ≫
          colimit.ι
            (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑↑(restrict X h))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj
              (restrict X h).presheaf)
            ((OpenNhds.map (ofRestrict X h).base x).op.obj (op V))) ≫
      (restrictStalkIso X h x).hom
[PROOFSTEP]
simp_rw [Category.assoc]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : OpenNhds (↑f x)
i : (IsOpenMap.functorNhds (_ : IsOpenMap ↑f) x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
  homOfLE (_ : ↑f '' (↑f ⁻¹' V.obj.1) ⊆ V.obj.1)
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
      (op V) =
    NatTrans.app
        (((whiskeringLeft (OpenNhds (↑(ofRestrict X h).base x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(ofRestrict X h).base x)).op).map
          (ofRestrict X h).c)
        (op V) ≫
      NatTrans.app
          (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (ofRestrict X h).base x).inv) (restrict X h).presheaf)
          (op V) ≫
        colimit.ι
            (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑↑(restrict X h))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj
              (restrict X h).presheaf)
            ((OpenNhds.map (ofRestrict X h).base x).op.obj (op V)) ≫
          (restrictStalkIso X h x).hom
[PROOFSTEP]
erw [colimit.ι_pre ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf) (h.isOpenMap.functorNhds x).op]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : OpenNhds (↑f x)
i : (IsOpenMap.functorNhds (_ : IsOpenMap ↑f) x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
  homOfLE (_ : ↑f '' (↑f ⁻¹' V.obj.1) ⊆ V.obj.1)
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
      (op V) =
    NatTrans.app
        (((whiskeringLeft (OpenNhds (↑(ofRestrict X h).base x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(ofRestrict X h).base x)).op).map
          (ofRestrict X h).c)
        (op V) ≫
      NatTrans.app
          (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (ofRestrict X h).base x).inv) (restrict X h).presheaf)
          (op V) ≫
        colimit.ι ((OpenNhds.inclusion (↑f x)).op ⋙ X.presheaf)
          ((IsOpenMap.functorNhds (_ : IsOpenMap ↑f) x).op.obj ((OpenNhds.map (ofRestrict X h).base x).op.obj (op V)))
[PROOFSTEP]
erw [← X.presheaf.map_comp_assoc]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : OpenNhds (↑f x)
i : (IsOpenMap.functorNhds (_ : IsOpenMap ↑f) x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
  homOfLE (_ : ↑f '' (↑f ⁻¹' V.obj.1) ⊆ V.obj.1)
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
      (op V) =
    X.presheaf.map
        ((NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑f)).counit
              ((OpenNhds.inclusion (↑(ofRestrict X h).base x)).op.obj (op V)).unop).op ≫
          (IsOpenMap.functor (_ : IsOpenMap ↑f)).op.map
            (NatTrans.app (NatTrans.op (OpenNhds.inclusionMapIso (ofRestrict X h).base x).inv) (op V))) ≫
      colimit.ι ((OpenNhds.inclusion (↑f x)).op ⋙ X.presheaf)
        ((IsOpenMap.functorNhds (_ : IsOpenMap ↑f) x).op.obj ((OpenNhds.map (ofRestrict X h).base x).op.obj (op V)))
[PROOFSTEP]
exact (colimit.w ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf) i.op).symm
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
⊢ IsIso (stalkMap (ofRestrict X h) x)
[PROOFSTEP]
rw [← restrictStalkIso_inv_eq_ofRestrict]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
⊢ IsIso (restrictStalkIso X h x).inv
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ stalkMap (𝟙 X) x = 𝟙 (stalk X x)
[PROOFSTEP]
dsimp [stalkMap]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C (↑(𝟙 ↑X) x)).map (𝟙 X).c ≫ stalkPushforward C (𝟙 ↑X) X.presheaf x = 𝟙 (stalk X x)
[PROOFSTEP]
simp only [stalkPushforward.id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C (↑(𝟙 ↑X) x)).map (𝟙 X).c ≫ (stalkFunctor C x).map (Pushforward.id X.presheaf).hom = 𝟙 (stalk X x)
[PROOFSTEP]
erw [← map_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C (↑(𝟙 ↑X) x)).map ((𝟙 X).c ≫ (Pushforward.id X.presheaf).hom) = 𝟙 (stalk X x)
[PROOFSTEP]
convert (stalkFunctor C x).map_id X.presheaf
[GOAL]
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
e_1✝ : (stalk X (↑(𝟙 ↑X) x) ⟶ stalk X x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)
⊢ (𝟙 X).c ≫ (Pushforward.id X.presheaf).hom = 𝟙 X.presheaf
[PROOFSTEP]
ext
[GOAL]
case h.e'_2.h.h.e'_8.w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
e_1✝ : (stalk X (↑(𝟙 ↑X) x) ⟶ stalk X x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)
U✝ : Opens ↑↑X
⊢ NatTrans.app ((𝟙 X).c ≫ (Pushforward.id X.presheaf).hom) (op U✝) = NatTrans.app (𝟙 X.presheaf) (op U✝)
[PROOFSTEP]
simp only [id_c, id_comp, Pushforward.id_hom_app, op_obj, eqToHom_refl, map_id]
[GOAL]
case h.e'_2.h.h.e'_8.w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
e_1✝ : (stalk X (↑(𝟙 ↑X) x) ⟶ stalk X x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)
U✝ : Opens ↑↑X
⊢ 𝟙 (X.presheaf.obj (op ((Opens.map (𝟙 ↑X)).obj (op U✝).unop))) = NatTrans.app (𝟙 X.presheaf) (op U✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
⊢ stalkMap (α ≫ β) x = stalkMap β (↑α.base x) ≫ stalkMap α x
[PROOFSTEP]
dsimp [stalkMap, stalkFunctor, stalkPushforward]
  -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
⊢ colimMap (whiskerLeft (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op (α ≫ β).c) ≫
      colimMap (whiskerRight (𝟙 (OpenNhds.map (α.base ≫ β.base) x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
        colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map (α.base ≫ β.base) x).op =
    (colimMap (whiskerLeft (OpenNhds.inclusion (↑β.base (↑α.base x))).op β.c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map β.base (↑α.base x) ⋙ OpenNhds.inclusion (↑α.base x)).op) Y.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion (↑α.base x)).op ⋙ Y.presheaf) (OpenNhds.map β.base (↑α.base x)).op) ≫
      colimMap (whiskerLeft (OpenNhds.inclusion (↑α.base x)).op α.c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map α.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map α.base x).op
[PROOFSTEP]
refine colimit.hom_ext fun U => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
U : (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        U ≫
      colimMap (whiskerLeft (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op (α ≫ β).c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map (α.base ≫ β.base) x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map (α.base ≫ β.base) x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        U ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑β.base (↑α.base x))).op β.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map β.base (↑α.base x) ⋙ OpenNhds.inclusion (↑α.base x)).op) Y.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion (↑α.base x)).op ⋙ Y.presheaf) (OpenNhds.map β.base (↑α.base x)).op) ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑α.base x)).op α.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map α.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map α.base x).op
[PROOFSTEP]
induction U with
| h U => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
U : (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        U ≫
      colimMap (whiskerLeft (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op (α ≫ β).c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map (α.base ≫ β.base) x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map (α.base ≫ β.base) x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        U ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑β.base (↑α.base x))).op β.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map β.base (↑α.base x) ⋙ OpenNhds.inclusion (↑α.base x)).op) Y.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion (↑α.base x)).op ⋙ Y.presheaf) (OpenNhds.map β.base (↑α.base x)).op) ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑α.base x)).op α.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map α.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map α.base x).op
[PROOFSTEP]
induction U with
| h U => ?_
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
U : OpenNhds (↑(α.base ≫ β.base) x)
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        (op U) ≫
      colimMap (whiskerLeft (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op (α ≫ β).c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map (α.base ≫ β.base) x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map (α.base ≫ β.base) x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        (op U) ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑β.base (↑α.base x))).op β.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map β.base (↑α.base x) ⋙ OpenNhds.inclusion (↑α.base x)).op) Y.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion (↑α.base x)).op ⋙ Y.presheaf) (OpenNhds.map β.base (↑α.base x)).op) ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑α.base x)).op α.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map α.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map α.base x).op
[PROOFSTEP]
cases U
[GOAL]
case h.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
obj✝ : Opens ↑↑Z
property✝ : ↑(α.base ≫ β.base) x ∈ obj✝
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        (op { obj := obj✝, property := property✝ }) ≫
      colimMap (whiskerLeft (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op (α ≫ β).c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map (α.base ≫ β.base) x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map (α.base ≫ β.base) x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        (op { obj := obj✝, property := property✝ }) ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑β.base (↑α.base x))).op β.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map β.base (↑α.base x) ⋙ OpenNhds.inclusion (↑α.base x)).op) Y.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion (↑α.base x)).op ⋙ Y.presheaf) (OpenNhds.map β.base (↑α.base x)).op) ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑α.base x)).op α.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map α.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map α.base x).op
[PROOFSTEP]
simp only [whiskeringLeft_obj_obj, comp_obj, op_obj, unop_op, OpenNhds.inclusion_obj, ι_colimMap_assoc,
  pushforwardObj_obj, Opens.map_comp_obj, whiskerLeft_app, comp_c_app, OpenNhds.map_obj, whiskerRight_app,
  NatTrans.id_app, map_id, colimit.ι_pre, id_comp, assoc, colimit.ι_pre_assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ stalk X x = stalk X x'
[PROOFSTEP]
rw [h₂]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ stalk Y (↑α.base x) = stalk Y (↑β.base x')
[PROOFSTEP]
rw [h₁, h₂]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X x') =
    eqToHom (_ : stalk Y (↑α.base x) = stalk Y (↑β.base x')) ≫ stalkMap β x'
[PROOFSTEP]
ext
[GOAL]
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
U✝ : Opens ↑↑Y
hxU✝ : ↑α.base x ∈ U✝
⊢ germ Y.presheaf { val := ↑α.base x, property := hxU✝ } ≫ stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X x') =
    germ Y.presheaf { val := ↑α.base x, property := hxU✝ } ≫
      eqToHom (_ : stalk Y (↑α.base x) = stalk Y (↑β.base x')) ≫ stalkMap β x'
[PROOFSTEP]
substs h₁ h₂
[GOAL]
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x : ↑↑X
U✝ : Opens ↑↑Y
hxU✝ : ↑α.base x ∈ U✝
⊢ germ Y.presheaf { val := ↑α.base x, property := hxU✝ } ≫ stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X x) =
    germ Y.presheaf { val := ↑α.base x, property := hxU✝ } ≫
      eqToHom (_ : stalk Y (↑α.base x) = stalk Y (↑α.base x)) ≫ stalkMap α x
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
x : ↑↑X
⊢ stalk Y (↑α.base x) = stalk Y (↑β.base x)
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
x : ↑↑X
⊢ stalkMap α x = eqToHom (_ : stalk Y (↑α.base x) = stalk Y (↑β.base x)) ≫ stalkMap β x
[PROOFSTEP]
rw [← stalkMap.congr α β h x x rfl, eqToHom_refl, Category.comp_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ stalk X x = stalk X x'
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ stalk Y (↑α.base x) = stalk Y (↑α.base x')
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X x') =
    eqToHom (_ : stalk Y (↑α.base x) = stalk Y (↑α.base x')) ≫ stalkMap α x'
[PROOFSTEP]
rw [stalkMap.congr α α rfl x x' h]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
⊢ ∃ inv, stalkMap α x ≫ inv = 𝟙 (stalk Y (↑α.base x)) ∧ inv ≫ stalkMap α x = 𝟙 (stalk X x)
[PROOFSTEP]
let β : Y ⟶ X := CategoryTheory.inv α
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
⊢ ∃ inv, stalkMap α x ≫ inv = 𝟙 (stalk Y (↑α.base x)) ∧ inv ≫ stalkMap α x = 𝟙 (stalk X x)
[PROOFSTEP]
have h_eq : (α ≫ β).base x = x := by
  rw [IsIso.hom_inv_id α, id_base, TopCat.id_app]
    -- Intuitively, the inverse of the stalk map of `α` at `x` should just be the stalk map of `β`
        -- at `α x`. Unfortunately, we have a problem with dependent type theory here: Because `x`
        -- is not *definitionally* equal to `β (α x)`, the map `stalk_map β (α x)` has not the correct
        -- type for an inverse.
        -- To get a proper inverse, we need to compose with the `eq_to_hom` arrow
        -- `X.stalk x ⟶ X.stalk ((α ≫ β).base x)`.
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
⊢ ↑(α ≫ β).base x = x
[PROOFSTEP]
rw [IsIso.hom_inv_id α, id_base, TopCat.id_app]
  -- Intuitively, the inverse of the stalk map of `α` at `x` should just be the stalk map of `β`
      -- at `α x`. Unfortunately, we have a problem with dependent type theory here: Because `x`
      -- is not *definitionally* equal to `β (α x)`, the map `stalk_map β (α x)` has not the correct
      -- type for an inverse.
      -- To get a proper inverse, we need to compose with the `eq_to_hom` arrow
      -- `X.stalk x ⟶ X.stalk ((α ≫ β).base x)`.
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : ↑(α ≫ β).base x = x
⊢ ∃ inv, stalkMap α x ≫ inv = 𝟙 (stalk Y (↑α.base x)) ∧ inv ≫ stalkMap α x = 𝟙 (stalk X x)
[PROOFSTEP]
refine' ⟨eqToHom (show X.stalk x = X.stalk ((α ≫ β).base x) by rw [h_eq]) ≫ (stalkMap β (α.base x) : _), _, _⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : ↑(α ≫ β).base x = x
⊢ stalk X x = stalk X (↑(α ≫ β).base x)
[PROOFSTEP]
rw [h_eq]
[GOAL]
case refine'_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : ↑(α ≫ β).base x = x
⊢ stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X (↑(α ≫ β).base x)) ≫ stalkMap β (↑α.base x) = 𝟙 (stalk Y (↑α.base x))
[PROOFSTEP]
rw [← Category.assoc, congr_point α x ((α ≫ β).base x) h_eq.symm, Category.assoc]
[GOAL]
case refine'_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : ↑(α ≫ β).base x = x
⊢ eqToHom (_ : stalk Y (↑α.base x) = stalk Y (↑α.base (↑(α ≫ β).base x))) ≫
      stalkMap α (↑(α ≫ β).base x) ≫ stalkMap β (↑α.base x) =
    𝟙 (stalk Y (↑α.base x))
[PROOFSTEP]
erw [← stalkMap.comp β α (α.base x)]
[GOAL]
case refine'_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : ↑(α ≫ β).base x = x
⊢ eqToHom (_ : stalk Y (↑α.base x) = stalk Y (↑α.base (↑(α ≫ β).base x))) ≫ stalkMap (β ≫ α) (↑α.base x) =
    𝟙 (stalk Y (↑α.base x))
[PROOFSTEP]
rw [congr_hom _ _ (IsIso.inv_hom_id α), stalkMap.id, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp]
[GOAL]
case refine'_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : ↑(α ≫ β).base x = x
⊢ (eqToHom (_ : stalk X x = stalk X (↑(α ≫ β).base x)) ≫ stalkMap β (↑α.base x)) ≫ stalkMap α x = 𝟙 (stalk X x)
[PROOFSTEP]
rw [Category.assoc, ← stalkMap.comp, congr_hom _ _ (IsIso.hom_inv_id α), stalkMap.id, eqToHom_trans_assoc, eqToHom_refl,
  Category.id_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
⊢ stalkSpecializes Y.presheaf (_ : ↑f.base x ⤳ ↑f.base y) ≫ stalkMap f x = stalkMap f y ≫ stalkSpecializes X.presheaf h
[PROOFSTEP]
dsimp [stalkSpecializes, stalkMap, stalkFunctor, stalkPushforward]
  -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
⊢ colimit.desc ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf)
        { pt := colimit ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf),
          ι :=
            NatTrans.mk fun U =>
              colimit.ι ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf)
                (op { obj := U.unop.obj, property := (_ : ↑f.base x ∈ U.unop.obj.carrier) }) } ≫
      colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base x)).op f.c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
    (colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base y)).op f.c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
      colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
        { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
          ι :=
            NatTrans.mk fun U =>
              colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                (op { obj := U.unop.obj, property := (_ : x ∈ U.unop.obj.carrier) }) }
[PROOFSTEP]
refine colimit.hom_ext fun j => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : (OpenNhds (↑f.base y))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds (↑f.base y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj (OpenNhds.inclusion (↑f.base y)).op).obj
          Y.presheaf)
        j ≫
      colimit.desc ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf)
          { pt := colimit ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf)
                  (op { obj := U.unop.obj, property := (_ : ↑f.base x ∈ U.unop.obj.carrier) }) } ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base x)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds (↑f.base y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj (OpenNhds.inclusion (↑f.base y)).op).obj
          Y.presheaf)
        j ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base y)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
        colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
          { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                  (op { obj := U.unop.obj, property := (_ : x ∈ U.unop.obj.carrier) }) }
[PROOFSTEP]
induction j with
| h j => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : (OpenNhds (↑f.base y))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds (↑f.base y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj (OpenNhds.inclusion (↑f.base y)).op).obj
          Y.presheaf)
        j ≫
      colimit.desc ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf)
          { pt := colimit ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf)
                  (op { obj := U.unop.obj, property := (_ : ↑f.base x ∈ U.unop.obj.carrier) }) } ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base x)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds (↑f.base y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj (OpenNhds.inclusion (↑f.base y)).op).obj
          Y.presheaf)
        j ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base y)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
        colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
          { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                  (op { obj := U.unop.obj, property := (_ : x ∈ U.unop.obj.carrier) }) }
[PROOFSTEP]
induction j with
| h j => ?_
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds (↑f.base y)
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds (↑f.base y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj (OpenNhds.inclusion (↑f.base y)).op).obj
          Y.presheaf)
        (op j) ≫
      colimit.desc ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf)
          { pt := colimit ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf)
                  (op { obj := U.unop.obj, property := (_ : ↑f.base x ∈ U.unop.obj.carrier) }) } ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base x)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds (↑f.base y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj (OpenNhds.inclusion (↑f.base y)).op).obj
          Y.presheaf)
        (op j) ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base y)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
        colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
          { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                  (op { obj := U.unop.obj, property := (_ : x ∈ U.unop.obj.carrier) }) }
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds (↑f.base y)
⊢ colimit.ι ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf) (op j) ≫
      colimit.desc ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf)
          { pt := colimit ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf)
                  (op { obj := U.unop.obj, property := (_ : ↑f.base x ∈ U.unop.obj.carrier) }) } ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base x)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
    colimit.ι ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf) (op j) ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base y)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
        colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
          { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                  (op { obj := U.unop.obj, property := (_ : x ∈ U.unop.obj.carrier) }) }
[PROOFSTEP]
simp only [colimit.ι_desc_assoc, comp_obj, op_obj, unop_op, ι_colimMap_assoc, colimit.map_desc, OpenNhds.inclusion_obj,
  pushforwardObj_obj, whiskerLeft_app, OpenNhds.map_obj, whiskerRight_app, NatTrans.id_app, map_id, colimit.ι_pre,
  id_comp, assoc, colimit.pre_desc]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds (↑f.base y)
⊢ NatTrans.app f.c (op j.obj) ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
        (op { obj := (Opens.map f.base).obj j.obj, property := (_ : ↑f.base x ∈ (op j).unop.obj.carrier) }) =
    colimit.ι ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf) (op j) ≫
      colimit.desc ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf)
        ((Cocones.precompose (whiskerLeft (OpenNhds.inclusion (↑f.base y)).op f.c)).obj
          ((Cocones.precompose (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf)).obj
            (Cocone.whisker (OpenNhds.map f.base y).op
              { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
                ι :=
                  NatTrans.mk fun U =>
                    colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                      (op { obj := U.unop.obj, property := (_ : x ∈ U.unop.obj.carrier) }) })))
[PROOFSTEP]
erw [colimit.ι_desc]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds (↑f.base y)
⊢ NatTrans.app f.c (op j.obj) ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
        (op { obj := (Opens.map f.base).obj j.obj, property := (_ : ↑f.base x ∈ (op j).unop.obj.carrier) }) =
    NatTrans.app
      ((Cocones.precompose (whiskerLeft (OpenNhds.inclusion (↑f.base y)).op f.c)).obj
          ((Cocones.precompose (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf)).obj
            (Cocone.whisker (OpenNhds.map f.base y).op
              { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
                ι :=
                  NatTrans.mk fun U =>
                    colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                      (op { obj := U.unop.obj, property := (_ : x ∈ U.unop.obj.carrier) }) }))).ι
      (op j)
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds (↑f.base y)
⊢ NatTrans.app f.c (op j.obj) ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
        (op { obj := (Opens.map f.base).obj j.obj, property := (_ : ↑f.base x ∈ (op j).unop.obj.carrier) }) =
    NatTrans.app f.c (op ((OpenNhds.inclusion (↑f.base y)).obj j)) ≫
      X.presheaf.map (𝟙 (op ((OpenNhds.inclusion y).obj ((OpenNhds.map f.base y).obj j)))) ≫
        colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
          (op
            { obj := ((OpenNhds.map f.base y).obj j).obj,
              property := (_ : x ∈ (op ((OpenNhds.map f.base y).obj j)).unop.obj.carrier) })
[PROOFSTEP]
erw [X.presheaf.map_id, id_comp]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds (↑f.base y)
⊢ NatTrans.app f.c (op j.obj) ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
        (op { obj := (Opens.map f.base).obj j.obj, property := (_ : ↑f.base x ∈ (op j).unop.obj.carrier) }) =
    NatTrans.app f.c (op ((OpenNhds.inclusion (↑f.base y)).obj j)) ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
        (op
          { obj := ((OpenNhds.map f.base y).obj j).obj,
            property := (_ : x ∈ (op ((OpenNhds.map f.base y).obj j)).unop.obj.carrier) })
[PROOFSTEP]
rfl
