-- Mathlib/Topology/Sheaves/Stalks.lean
theorem id (ℱ : X.Presheaf C) (x : X) :
    ℱ.stalkPushforward C (𝟙 X) x = (stalkFunctor C x).map (Pushforward.id ℱ).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
ℱ : Presheaf C X
x : ↑X
⊢ stalkPushforward C (𝟙 X) ℱ x = (stalkFunctor C x).map (Pushforward.id ℱ).hom

Tactic:
ext

Result:
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
ℱ : Presheaf C X
x : ↑X
U✝ : Opens ↑X
hxU✝ : (ConcreteCategory.hom (𝟙 X)) x ∈ U✝
⊢ ((pushforward C (𝟙 X)).obj ℱ).germ U✝ ((ConcreteCategory.hom (𝟙 X)) x) hxU✝ ≫ stalkPushforward C (𝟙 X) ℱ x =
    ((pushforward C (𝟙 X)).obj ℱ).germ U✝ ((ConcreteCategory.hom (𝟙 X)) x) hxU✝ ≫
      (stalkFunctor C x).map (Pushforward.id ℱ).hom

Proof state:
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
ℱ : Presheaf C X
x : ↑X
U✝ : Opens ↑X
hxU✝ : (ConcreteCategory.hom (𝟙 X)) x ∈ U✝
⊢ 𝟙
        (ℱ.obj
          ((OpenNhds.inclusion ((ConcreteCategory.hom (𝟙 X)) x) ⋙ Opens.map (𝟙 X)).op.obj
            (op { obj := U✝, property := hxU✝ }))) ≫
      colimit.ι
          ((OpenNhds.map (𝟙 X) x).op ⋙
            ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ)
          (op { obj := U✝, property := hxU✝ }) ≫
        colimit.pre (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ)
          (OpenNhds.map (𝟙 X) x).op =
    colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom (𝟙 X)) x)).op ⋙ (pushforward C (𝟙 X)).obj ℱ)
        (op { obj := U✝, property := hxU✝ }) ≫
      (stalkFunctor C x).map (Pushforward.id ℱ).hom

Tactic:
simp [stalkFunctor]

Result:
no goals

Proof state:
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
ℱ : Presheaf C X
x : ↑X
U✝ : Opens ↑X
hxU✝ : (ConcreteCategory.hom (𝟙 X)) x ∈ U✝
⊢ ((pushforward C (𝟙 X)).obj ℱ).germ U✝ ((ConcreteCategory.hom (𝟙 X)) x) hxU✝ ≫ stalkPushforward C (𝟙 X) ℱ x =
    ((pushforward C (𝟙 X)).obj ℱ).germ U✝ ((ConcreteCategory.hom (𝟙 X)) x) hxU✝ ≫
      (stalkFunctor C x).map (Pushforward.id ℱ).hom

Tactic:
simp only [stalkPushforward, germ, colim_map, ι_colimMap_assoc, whiskerRight_app]

Result:
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
ℱ : Presheaf C X
x : ↑X
U✝ : Opens ↑X
hxU✝ : (ConcreteCategory.hom (𝟙 X)) x ∈ U✝
⊢ ℱ.map ((NatTrans.op (OpenNhds.inclusionMapIso (𝟙 X) x).inv).app (op { obj := U✝, property := hxU✝ })) ≫
      colimit.ι
          ((OpenNhds.map (𝟙 X) x).op ⋙
            ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ)
          (op { obj := U✝, property := hxU✝ }) ≫
        colimit.pre (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ)
          (OpenNhds.map (𝟙 X) x).op =
    colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom (𝟙 X)) x)).op ⋙ (pushforward C (𝟙 X)).obj ℱ)
        (op { obj := U✝, property := hxU✝ }) ≫
      (stalkFunctor C x).map (Pushforward.id ℱ).hom

Proof state:
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
ℱ : Presheaf C X
x : ↑X
U✝ : Opens ↑X
hxU✝ : (ConcreteCategory.hom (𝟙 X)) x ∈ U✝
⊢ ℱ.map ((NatTrans.op (OpenNhds.inclusionMapIso (𝟙 X) x).inv).app (op { obj := U✝, property := hxU✝ })) ≫
      colimit.ι
          ((OpenNhds.map (𝟙 X) x).op ⋙
            ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ)
          (op { obj := U✝, property := hxU✝ }) ≫
        colimit.pre (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ)
          (OpenNhds.map (𝟙 X) x).op =
    colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom (𝟙 X)) x)).op ⋙ (pushforward C (𝟙 X)).obj ℱ)
        (op { obj := U✝, property := hxU✝ }) ≫
      (stalkFunctor C x).map (Pushforward.id ℱ).hom

Tactic:
erw [CategoryTheory.Functor.map_id]

Result:
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
ℱ : Presheaf C X
x : ↑X
U✝ : Opens ↑X
hxU✝ : (ConcreteCategory.hom (𝟙 X)) x ∈ U✝
⊢ 𝟙
        (ℱ.obj
          ((OpenNhds.inclusion ((ConcreteCategory.hom (𝟙 X)) x) ⋙ Opens.map (𝟙 X)).op.obj
            (op { obj := U✝, property := hxU✝ }))) ≫
      colimit.ι
          ((OpenNhds.map (𝟙 X) x).op ⋙
            ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ)
          (op { obj := U✝, property := hxU✝ }) ≫
        colimit.pre (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ)
          (OpenNhds.map (𝟙 X) x).op =
    colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom (𝟙 X)) x)).op ⋙ (pushforward C (𝟙 X)).obj ℱ)
        (op { obj := U✝, property := hxU✝ }) ≫
      (stalkFunctor C x).map (Pushforward.id ℱ).hom