-- Mathlib/Topology/Sheaves/Stalks.lean
theorem stalkSpecializes_stalkPushforward (f : X ⟶ Y) (F : X.Presheaf C) {x y : X} (h : x ⤳ y) :
    (f _* F).stalkSpecializes (f.hom.map_specializes h) ≫ F.stalkPushforward _ f x =
      F.stalkPushforward _ f y ≫ F.stalkSpecializes h

Proof state:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C X
x y : ↑X
h : x ⤳ y
j✝ : (OpenNhds ((Hom.hom f) y))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((Hom.hom f) y))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj (OpenNhds.inclusion ((Hom.hom f) y)).op).obj
          ((pushforward C f).obj F))
        j✝ ≫
      ((pushforward C f).obj F).stalkSpecializes ⋯ ≫
        colim.map (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f x).inv) F) ≫
          colimit.pre (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F)
            (OpenNhds.map f x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((Hom.hom f) y))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj (OpenNhds.inclusion ((Hom.hom f) y)).op).obj
          ((pushforward C f).obj F))
        j✝ ≫
      (colim.map (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f y).inv) F) ≫
          colimit.pre (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion y).op).obj F)
            (OpenNhds.map f y).op) ≫
        F.stalkSpecializes h

Tactic:
simp only [stalkSpecializes, colimit.ι_desc_assoc, colimit.ι_map_assoc, colimit.ι_pre,
  Category.assoc, colimit.pre_desc, colimit.ι_desc]

Result:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C X
x y : ↑X
h : x ⤳ y
j✝ : (OpenNhds ((Hom.hom f) y))ᵒᵖ
⊢ (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f x).inv) F).app (op { obj := (unop j✝).obj, property := ⋯ }) ≫
      colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F)
        ((OpenNhds.map f x).op.obj (op { obj := (unop j✝).obj, property := ⋯ })) =
    (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f y).inv) F).app j✝ ≫
      (Cocone.whisker (OpenNhds.map f y).op
              { pt := (stalkFunctor C x).toPrefunctor.1 F,
                ι :=
                  {
                    app := fun U =>
                      colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op { obj := (unop U).obj, property := ⋯ }),
                    naturality := ⋯ } }).ι.app
        j✝

Proof state:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C X
x y : ↑X
h : x ⤳ y
j✝ : (OpenNhds ((Hom.hom f) y))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((Hom.hom f) y))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj (OpenNhds.inclusion ((Hom.hom f) y)).op).obj
          ((pushforward C f).obj F))
        j✝ ≫
      ((pushforward C f).obj F).stalkSpecializes ⋯ ≫ stalkPushforward C f F x =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((Hom.hom f) y))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj (OpenNhds.inclusion ((Hom.hom f) y)).op).obj
          ((pushforward C f).obj F))
        j✝ ≫
      stalkPushforward C f F y ≫ F.stalkSpecializes h

Tactic:
delta stalkPushforward

Result:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C X
x y : ↑X
h : x ⤳ y
j✝ : (OpenNhds ((Hom.hom f) y))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((Hom.hom f) y))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj (OpenNhds.inclusion ((Hom.hom f) y)).op).obj
          ((pushforward C f).obj F))
        j✝ ≫
      ((pushforward C f).obj F).stalkSpecializes ⋯ ≫
        colim.map (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f x).inv) F) ≫
          colimit.pre (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F)
            (OpenNhds.map f x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((Hom.hom f) y))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj (OpenNhds.inclusion ((Hom.hom f) y)).op).obj
          ((pushforward C f).obj F))
        j✝ ≫
      (colim.map (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f y).inv) F) ≫
          colimit.pre (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion y).op).obj F)
            (OpenNhds.map f y).op) ≫
        F.stalkSpecializes h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C X
x y : ↑X
h : x ⤳ y
⊢ ((pushforward C f).obj F).stalkSpecializes ⋯ ≫ stalkPushforward C f F x =
    stalkPushforward C f F y ≫ F.stalkSpecializes h

Tactic:
ext

Result:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C X
x y : ↑X
h : x ⤳ y
j✝ : (OpenNhds ((Hom.hom f) y))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((Hom.hom f) y))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj (OpenNhds.inclusion ((Hom.hom f) y)).op).obj
          ((pushforward C f).obj F))
        j✝ ≫
      ((pushforward C f).obj F).stalkSpecializes ⋯ ≫ stalkPushforward C f F x =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((Hom.hom f) y))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj (OpenNhds.inclusion ((Hom.hom f) y)).op).obj
          ((pushforward C f).obj F))
        j✝ ≫
      stalkPushforward C f F y ≫ F.stalkSpecializes h

Proof state:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C X
x y : ↑X
h : x ⤳ y
j✝ : (OpenNhds ((Hom.hom f) y))ᵒᵖ
⊢ (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f x).inv) F).app (op { obj := (unop j✝).obj, property := ⋯ }) ≫
      colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F)
        ((OpenNhds.map f x).op.obj (op { obj := (unop j✝).obj, property := ⋯ })) =
    (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f y).inv) F).app j✝ ≫
      (Cocone.whisker (OpenNhds.map f y).op
              { pt := (stalkFunctor C x).toPrefunctor.1 F,
                ι :=
                  {
                    app := fun U =>
                      colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op { obj := (unop U).obj, property := ⋯ }),
                    naturality := ⋯ } }).ι.app
        j✝

Tactic:
rfl

Result:
no goals