-- Mathlib/Geometry/RingedSpace/Stalks.lean
theorem comp {X Y Z : PresheafedSpace.{_, _, v} C} (α : X ⟶ Y) (β : Y ⟶ Z) (x : X) :
    (α ≫ β).stalkMap x =
      (β.stalkMap (α.base x) : Z.presheaf.stalk (β.base (α.base x)) ⟶ Y.presheaf.stalk (α.base x)) ≫
        (α.stalkMap x : Y.presheaf.stalk (α.base x) ⟶ X.presheaf.stalk x)

Proof state:
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 ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.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 ((ConcreteCategory.hom β.base) ((ConcreteCategory.hom α.base) x))).op β.c) ≫
        colimMap
            (whiskerRight
              (𝟙
                (OpenNhds.map β.base ((ConcreteCategory.hom α.base) x) ⋙
                    OpenNhds.inclusion ((ConcreteCategory.hom α.base) x)).op)
              Y.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion ((ConcreteCategory.hom α.base) x)).op ⋙ Y.presheaf)
            (OpenNhds.map β.base ((ConcreteCategory.hom α.base) x)).op) ≫
      colimMap (whiskerLeft (OpenNhds.inclusion ((ConcreteCategory.hom α.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

Tactic:
apply colimit.hom_ext

Result:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
⊢ ∀ (j : (OpenNhds ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x)))ᵒᵖ),
    colimit.ι
          (((whiskeringLeft (OpenNhds ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x)))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
                (OpenNhds.inclusion ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x))).op).obj
            Z.presheaf)
          j ≫
        colimMap (whiskerLeft (OpenNhds.inclusion ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.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 ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x)))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
                (OpenNhds.inclusion ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x))).op).obj
            Z.presheaf)
          j ≫
        (colimMap
              (whiskerLeft (OpenNhds.inclusion ((ConcreteCategory.hom β.base) ((ConcreteCategory.hom α.base) x))).op
                β.c) ≫
            colimMap
                (whiskerRight
                  (𝟙
                    (OpenNhds.map β.base ((ConcreteCategory.hom α.base) x) ⋙
                        OpenNhds.inclusion ((ConcreteCategory.hom α.base) x)).op)
                  Y.presheaf) ≫
              colimit.pre ((OpenNhds.inclusion ((ConcreteCategory.hom α.base) x)).op ⋙ Y.presheaf)
                (OpenNhds.map β.base ((ConcreteCategory.hom α.base) x)).op) ≫
          colimMap (whiskerLeft (OpenNhds.inclusion ((ConcreteCategory.hom α.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

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
⊢ Hom.stalkMap (α ≫ β) x = Hom.stalkMap β ((ConcreteCategory.hom α.base) x) ≫ Hom.stalkMap α x

Tactic:
dsimp [Hom.stalkMap, stalkFunctor, stalkPushforward]

Result:
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 ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.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 ((ConcreteCategory.hom β.base) ((ConcreteCategory.hom α.base) x))).op β.c) ≫
        colimMap
            (whiskerRight
              (𝟙
                (OpenNhds.map β.base ((ConcreteCategory.hom α.base) x) ⋙
                    OpenNhds.inclusion ((ConcreteCategory.hom α.base) x)).op)
              Y.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion ((ConcreteCategory.hom α.base) x)).op ⋙ Y.presheaf)
            (OpenNhds.map β.base ((ConcreteCategory.hom α.base) x)).op) ≫
      colimMap (whiskerLeft (OpenNhds.inclusion ((ConcreteCategory.hom α.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