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
⊢ ∀ (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

Tactic:
rintro ⟨U, hU⟩

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
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 ⟨U, hU⟩) ≫
      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)
        (op ⟨U, hU⟩) ≫
      (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