-- Mathlib/Topology/Sheaves/Stalks.lean
theorem stalkSpecializes_stalkFunctor_map {F G : X.Presheaf C} (f : F ⟶ G) {x y : X} (h : x ⤳ y) :
    F.stalkSpecializes h ≫ (stalkFunctor C x).map f =
      (stalkFunctor C y).map f ≫ G.stalkSpecializes h

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

Tactic:
ext

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

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

Tactic:
simpa [stalkSpecializes] using by rfl

Result:
no goals

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

Tactic:
delta stalkFunctor

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

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F G : Presheaf C X
f : F ⟶ G
x y : ↑X
h : x ⤳ y
j✝ : (OpenNhds y)ᵒᵖ
⊢ f.app (op (unop j✝).obj) ≫ colimit.ι ((OpenNhds.inclusion x).op ⋙ G) (op { obj := (unop j✝).obj, property := ⋯ }) =
    f.app (op ((OpenNhds.inclusion y).obj (unop j✝))) ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ G) (op { obj := (unop j✝).obj, property := ⋯ })

Tactic:
rfl

Result:
no goals