Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
⊢ colimMap ((OpenNhds.inclusion ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x))).op.whiskerLeft (α ≫ β).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
          ((OpenNhds.inclusion ((ConcreteCategory.hom β.base) ((ConcreteCategory.hom α.base) x))).op.whiskerLeft β.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 ((OpenNhds.inclusion ((ConcreteCategory.hom α.base) x)).op.whiskerLeft α.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

Goal state after:
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 ((OpenNhds.inclusion ((TopCat.Hom.hom β.base) ((TopCat.Hom.hom α.base) x))).op.whiskerLeft (α ≫ β).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
              ((OpenNhds.inclusion ((ConcreteCategory.hom β.base) ((ConcreteCategory.hom α.base) x))).op.whiskerLeft
                β.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 ((OpenNhds.inclusion ((ConcreteCategory.hom α.base) x)).op.whiskerLeft α.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