-- Module: Mathlib.Geometry.RingedSpace.Stalks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y Z : PresheafedSpace.{v, u, v} C
α : X ⟶ Y
β : Y ⟶ Z
x : (↑(↑X : TopCat) : Type v)
dsimp :
  Eq (α :=
    Z.presheaf.stalk
        ((TopCat.Hom.hom β.base : (a : (↑(↑Y : TopCat) : Type v)) → (↑(↑Z : TopCat) : Type v))
          ((TopCat.Hom.hom α.base : (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v)) x :
            (↑(↑Y : TopCat) : Type v))) ⟶
      X.presheaf.stalk x)
    (CategoryStruct.comp (Y :=
      colimit (J :=
        (OpenNhds (X := (↑Z : TopCat))
            ((TopCat.Hom.hom β.base : (a : (↑(↑Y : TopCat) : Type v)) → (↑(↑Z : TopCat) : Type v))
              ((TopCat.Hom.hom α.base : (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v)) x :
                (↑(↑Y : TopCat) : Type v))))ᵒᵖ)
        (Functor.op
            (OpenNhds.inclusion
              ((TopCat.Hom.hom β.base : (a : (↑(↑Y : TopCat) : Type v)) → (↑(↑Z : TopCat) : Type v))
                ((TopCat.Hom.hom α.base : (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v)) x :
                  (↑(↑Y : TopCat) : Type v)))) ⋙
          obj (pushforward C (α.base ≫ β.base)) X.presheaf))
      (colimMap
        (whiskerLeft
          (Functor.op
            (OpenNhds.inclusion
              ((TopCat.Hom.hom β.base : (a : (↑(↑Y : TopCat) : Type v)) → (↑(↑Z : TopCat) : Type v))
                ((TopCat.Hom.hom α.base : (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v)) x :
                  (↑(↑Y : TopCat) : Type v)))))
          (α ≫ β).c))
      (CategoryStruct.comp (Y :=
        colimit ((OpenNhds.map (α.base ≫ β.base) x).op ⋙ (OpenNhds.inclusion x).op ⋙ X.presheaf))
        (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)))
    (CategoryStruct.comp (Y :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x))
      (CategoryStruct.comp (Y :=
        colimit (J :=
          (OpenNhds (X := (↑Z : TopCat))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) β.base :
                  (a : (↑(↑Y : TopCat) : Type v)) → (↑(↑Z : TopCat) : Type v))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) α.base :
                      (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                    x :
                  (↑(↑Y : TopCat) : Type v))))ᵒᵖ)
          (Functor.op
              (OpenNhds.inclusion
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) β.base :
                    (a : (↑(↑Y : TopCat) : Type v)) → (↑(↑Z : TopCat) : Type v))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) α.base :
                        (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                      x :
                    (↑(↑Y : TopCat) : Type v)))) ⋙
            obj (pushforward C β.base) Y.presheaf))
        (colimMap
          (whiskerLeft
            (Functor.op
              (OpenNhds.inclusion
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) β.base :
                    (a : (↑(↑Y : TopCat) : Type v)) → (↑(↑Z : TopCat) : Type v))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) α.base :
                        (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                      x :
                    (↑(↑Y : TopCat) : Type v)))))
            β.c))
        (CategoryStruct.comp (Y :=
          colimit (J :=
            (OpenNhds (X := (↑Z : TopCat))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) β.base :
                    (a : (↑(↑Y : TopCat) : Type v)) → (↑(↑Z : TopCat) : Type v))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) α.base :
                        (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                      x :
                    (↑(↑Y : TopCat) : Type v))))ᵒᵖ)
            (Functor.op
                (OpenNhds.map β.base
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) α.base :
                      (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                    x)) ⋙
              Functor.op
                  (OpenNhds.inclusion
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) α.base :
                        (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                      x)) ⋙
                Y.presheaf))
          (colimMap
            (whiskerRight
              (𝟙
                (Functor.op
                  (OpenNhds.map β.base
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                            TopCat.carrier) α.base :
                          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                        x) ⋙
                    OpenNhds.inclusion
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                            TopCat.carrier) α.base :
                          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                        x))))
              Y.presheaf))
          (colimit.pre
            (Functor.op
                (OpenNhds.inclusion
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) α.base :
                      (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                    x)) ⋙
              Y.presheaf)
            (Functor.op
              (OpenNhds.map β.base
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) α.base :
                    (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                  x))))))
      (CategoryStruct.comp (Y :=
        colimit (J :=
          (OpenNhds (X := (↑Y : TopCat))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) α.base :
                  (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                x))ᵒᵖ)
          (Functor.op
              (OpenNhds.inclusion
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) α.base :
                    (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                  x)) ⋙
            obj (pushforward C α.base) X.presheaf))
        (colimMap
          (whiskerLeft
            (Functor.op
              (OpenNhds.inclusion
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) α.base :
                    (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
                  x)))
            α.c))
        (CategoryStruct.comp (Y := colimit ((OpenNhds.map α.base x).op ⋙ (OpenNhds.inclusion x).op ⋙ X.presheaf))
          (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))))
⊢ Eq (α :=
    Z.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (α ≫ β).base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Z : TopCat) : Type v))
          x) ⟶
      X.presheaf.stalk x)
    (Hom.stalkMap (α ≫ β) x)
    (Hom.stalkMap β
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              α.base :
            (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
          x) ≫
      Hom.stalkMap α x)

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

Premises used: AlgebraicGeometry.PresheafedSpace.Hom.stalkMap, TopCat.Presheaf.stalkFunctor, TopCat.Presheaf.stalkPushforward