-- Mathlib/Geometry/RingedSpace/Stalks.lean
theorem stalkSpecializes_stalkMap {X Y : PresheafedSpace.{_, _, v} C}
    (f : X ⟶ Y) {x y : X} (h : x ⤳ y) :
    Y.presheaf.stalkSpecializes (f.base.hom.map_specializes h) ≫ f.stalkMap x =
      f.stalkMap y ≫ X.presheaf.stalkSpecializes h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : (OpenNhds ((TopCat.Hom.hom f.base) y))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((TopCat.Hom.hom f.base) y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj
              (OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op).obj
          Y.presheaf)
        j ≫
      colimit.desc ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op ⋙ Y.presheaf)
          { pt := colimit ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) x)).op ⋙ Y.presheaf),
            ι :=
              {
                app := fun U =>
                  colimit.ι ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) x)).op ⋙ Y.presheaf)
                    (op { obj := (unop U).obj, property := ⋯ }),
                naturality := ⋯ } } ≫
        colimMap (whiskerLeft (OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((TopCat.Hom.hom f.base) y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj
              (OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op).obj
          Y.presheaf)
        j ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion ((ConcreteCategory.hom f.base) y)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
        colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
          { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
            ι :=
              {
                app := fun U =>
                  colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf) (op { obj := (unop U).obj, property := ⋯ }),
                naturality := ⋯ } }

Tactic:
induction j with | h j => ?_

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds ((TopCat.Hom.hom f.base) y)
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((TopCat.Hom.hom f.base) y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj
              (OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op).obj
          Y.presheaf)
        (op j) ≫
      colimit.desc ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op ⋙ Y.presheaf)
          { pt := colimit ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) x)).op ⋙ Y.presheaf),
            ι :=
              {
                app := fun U =>
                  colimit.ι ((OpenNhds.inclusion ((TopCat.Hom.hom f.base) x)).op ⋙ Y.presheaf)
                    (op { obj := (unop U).obj, property := ⋯ }),
                naturality := ⋯ } } ≫
        colimMap (whiskerLeft (OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((TopCat.Hom.hom f.base) y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj
              (OpenNhds.inclusion ((TopCat.Hom.hom f.base) y)).op).obj
          Y.presheaf)
        (op j) ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion ((ConcreteCategory.hom f.base) y)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
        colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
          { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
            ι :=
              {
                app := fun U =>
                  colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf) (op { obj := (unop U).obj, property := ⋯ }),
                naturality := ⋯ } }

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds ((TopCat.Hom.hom f.base) y)
⊢ f.c.app ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) x)).op.obj (op { obj := j.obj, property := ⋯ })) ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
        ((OpenNhds.map f.base x).op.obj (op { obj := j.obj, property := ⋯ })) =
    f.c.app ((OpenNhds.inclusion ((ConcreteCategory.hom f.base) y)).op.obj (op j)) ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
        ((OpenNhds.map f.base x).op.obj (op { obj := j.obj, property := ⋯ }))

Tactic:
rfl

Result:
no goals