-- 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:
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

Tactic:
rintro ⟨U, hU⟩

Result:
case w.op.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
U : Opens ↑↑Z
hU : (TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x) ∈ U
⊢ 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)
        (op { obj := U, property := hU }) ≫
      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)
        (op { obj := U, property := hU }) ≫
      (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:
case w.op.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
U : Opens ↑↑Z
hU : (TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x) ∈ U
⊢ 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)
        (op { obj := U, property := hU }) ≫
      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)
        (op { obj := U, property := hU }) ≫
      (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:
simp

Result:
no goals