C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
F : Presheaf C X
U : Opens ↑Y
x : { x // x ∈ (Opens.map f).obj U }
⊢ F.map
        ((NatTrans.op (OpenNhds.inclusionMapIso f ↑x).inv).app
          { obj := U,
              property :=
                (_ : ↑{ val := (forget TopCat).map f ↑x, property := (_ : ↑x ∈ (Opens.map f).obj U) } ∈ U) }.op) ≫
      colimit.ι (((whiskeringLeft (OpenNhds ↑x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion ↑x))).obj F)
        ((Functor.op (OpenNhds.map f ↑x)).obj
          { obj := U,
              property :=
                (_ : ↑{ val := (forget TopCat).map f ↑x, property := (_ : ↑x ∈ (Opens.map f).obj U) } ∈ U) }.op) =
    germ F x
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
F : Presheaf C X
U : Opens ↑Y
x : { x // x ∈ (Opens.map f).obj U }
⊢ germ (f _* F) { val := (forget TopCat).map f ↑x, property := (_ : ↑x ∈ (Opens.map f).obj U) } ≫
      stalkPushforward C f F ↑x =
    germ F x
rw [stalkPushforward, germ, colimit.ι_map_assoc, colimit.ι_pre, whiskerRight_app]
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
F : Presheaf C X
U : Opens ↑Y
x : { x // x ∈ (Opens.map f).obj U }
⊢ colimit.ι (((whiskeringLeft (OpenNhds ↑x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion ↑x))).obj F)
      ((Functor.op (OpenNhds.map f ↑x)).obj
        { obj := U,
            property :=
              (_ : ↑{ val := (forget TopCat).map f ↑x, property := (_ : ↑x ∈ (Opens.map f).obj U) } ∈ U) }.op) =
    germ F x
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
F : Presheaf C X
U : Opens ↑Y
x : { x // x ∈ (Opens.map f).obj U }
⊢ F.map
        ((NatTrans.op (OpenNhds.inclusionMapIso f ↑x).inv).app
          { obj := U,
              property :=
                (_ : ↑{ val := (forget TopCat).map f ↑x, property := (_ : ↑x ∈ (Opens.map f).obj U) } ∈ U) }.op) ≫
      colimit.ι (((whiskeringLeft (OpenNhds ↑x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion ↑x))).obj F)
        ((Functor.op (OpenNhds.map f ↑x)).obj
          { obj := U,
              property :=
                (_ : ↑{ val := (forget TopCat).map f ↑x, property := (_ : ↑x ∈ (Opens.map f).obj U) } ∈ U) }.op) =
    germ F x
erw [CategoryTheory.Functor.map_id, Category.id_comp]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
f : X ⟶ Y
F : Presheaf C X
U : Opens ↑Y
x : { x // x ∈ (Opens.map f).obj U }
⊢ colimit.ι (((whiskeringLeft (OpenNhds ↑x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Functor.op (OpenNhds.inclusion ↑x))).obj F)
      ((Functor.op (OpenNhds.map f ↑x)).obj
        { obj := U,
            property :=
              (_ : ↑{ val := (forget TopCat).map f ↑x, property := (_ : ↑x ∈ (Opens.map f).obj U) } ∈ U) }.op) =
    germ F x
rfl