C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ stalkPushforward C (f ≫ g) ℱ x = stalkPushforward C g (f _* ℱ) ((forget TopCat).map f x) ≫ stalkPushforward C f ℱ x
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ stalkPushforward C (f ≫ g) ℱ x = stalkPushforward C g (f _* ℱ) ((forget TopCat).map f x) ≫ stalkPushforward C f ℱ x
change (_ : colimit _ ⟶  _) = (_ : colimit _ ⟶  _)
case w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
U : (OpenNhds ((forget TopCat).map (f ≫ g) x))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map (f ≫ g) x))ᵒᵖ (Opens ↑Z)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map (f ≫ g) x)))).obj
          ((f ≫ g) _* ℱ))
        U ≫
      stalkPushforward C (f ≫ g) ℱ x =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map (f ≫ g) x))ᵒᵖ (Opens ↑Z)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map (f ≫ g) x)))).obj
          ((f ≫ g) _* ℱ))
        U ≫
      stalkPushforward C g (f _* ℱ) ((forget TopCat).map f x) ≫ stalkPushforward C f ℱ x
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ stalkPushforward C (f ≫ g) ℱ x = stalkPushforward C g (f _* ℱ) ((forget TopCat).map f x) ≫ stalkPushforward C f ℱ x
ext U
case w.mk.mk.mk
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
carrier✝ : Set ↑Z
is_open'✝ : IsOpen carrier✝
property✝ : (forget TopCat).map (f ≫ g) x ∈ { carrier := carrier✝, is_open' := is_open'✝ }
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map (f ≫ g) x))ᵒᵖ (Opens ↑Z)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map (f ≫ g) x)))).obj
          ((f ≫ g) _* ℱ))
        { unop := { obj := { carrier := carrier✝, is_open' := is_open'✝ }, property := property✝ } } ≫
      stalkPushforward C (f ≫ g) ℱ x =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map (f ≫ g) x))ᵒᵖ (Opens ↑Z)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map (f ≫ g) x)))).obj
          ((f ≫ g) _* ℱ))
        { unop := { obj := { carrier := carrier✝, is_open' := is_open'✝ }, property := property✝ } } ≫
      stalkPushforward C g (f _* ℱ) ((forget TopCat).map f x) ≫ stalkPushforward C f ℱ x
case w
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
U : (OpenNhds ((forget TopCat).map (f ≫ g) x))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map (f ≫ g) x))ᵒᵖ (Opens ↑Z)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map (f ≫ g) x)))).obj
          ((f ≫ g) _* ℱ))
        U ≫
      stalkPushforward C (f ≫ g) ℱ x =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map (f ≫ g) x))ᵒᵖ (Opens ↑Z)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map (f ≫ g) x)))).obj
          ((f ≫ g) _* ℱ))
        U ≫
      stalkPushforward C g (f _* ℱ) ((forget TopCat).map f x) ≫ stalkPushforward C f ℱ x
rcases U with ⟨⟨_, _⟩, _⟩
case w.mk.mk.mk
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
carrier✝ : Set ↑Z
is_open'✝ : IsOpen carrier✝
property✝ : (forget TopCat).map (f ≫ g) x ∈ { carrier := carrier✝, is_open' := is_open'✝ }
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map (f ≫ g) x))ᵒᵖ (Opens ↑Z)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map (f ≫ g) x)))).obj
          ((f ≫ g) _* ℱ))
        { unop := { obj := { carrier := carrier✝, is_open' := is_open'✝ }, property := property✝ } } ≫
      stalkPushforward C (f ≫ g) ℱ x =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map (f ≫ g) x))ᵒᵖ (Opens ↑Z)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map (f ≫ g) x)))).obj
          ((f ≫ g) _* ℱ))
        { unop := { obj := { carrier := carrier✝, is_open' := is_open'✝ }, property := property✝ } } ≫
      stalkPushforward C g (f _* ℱ) ((forget TopCat).map f x) ≫ stalkPushforward C f ℱ x
case w.mk.mk.mk
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
carrier✝ : Set ↑Z
is_open'✝ : IsOpen carrier✝
property✝ : (forget TopCat).map (f ≫ g) x ∈ { carrier := carrier✝, is_open' := is_open'✝ }
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map (f ≫ g) x))ᵒᵖ (Opens ↑Z)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map (f ≫ g) x)))).obj
          ((f ≫ g) _* ℱ))
        { unop := { obj := { carrier := carrier✝, is_open' := is_open'✝ }, property := property✝ } } ≫
      stalkPushforward C (f ≫ g) ℱ x =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map (f ≫ g) x))ᵒᵖ (Opens ↑Z)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map (f ≫ g) x)))).obj
          ((f ≫ g) _* ℱ))
        { unop := { obj := { carrier := carrier✝, is_open' := is_open'✝ }, property := property✝ } } ≫
      stalkPushforward C g (f _* ℱ) ((forget TopCat).map f x) ≫ stalkPushforward C f ℱ x
simp only [colimit.ι_map_assoc, colimit.ι_pre_assoc, whiskerRight_app, Category.assoc]
no goals
case w.mk.mk.mk
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
carrier✝ : Set ↑Z
is_open'✝ : IsOpen carrier✝
property✝ : (forget TopCat).map (f ≫ g) x ∈ { carrier := carrier✝, is_open' := is_open'✝ }
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map (f ≫ g) x))ᵒᵖ (Opens ↑Z)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map (f ≫ g) x)))).obj
          ((f ≫ g) _* ℱ))
        { unop := { obj := { carrier := carrier✝, is_open' := is_open'✝ }, property := property✝ } } ≫
      stalkPushforward C (f ≫ g) ℱ x =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((forget TopCat).map (f ≫ g) x))ᵒᵖ (Opens ↑Z)ᵒᵖ C).obj
              (Functor.op (OpenNhds.inclusion ((forget TopCat).map (f ≫ g) x)))).obj
          ((f ≫ g) _* ℱ))
        { unop := { obj := { carrier := carrier✝, is_open' := is_open'✝ }, property := property✝ } } ≫
      stalkPushforward C g (f _* ℱ) ((forget TopCat).map f x) ≫ stalkPushforward C f ℱ x
simp [stalkFunctor, stalkPushforward]