-- Mathlib/Geometry/RingedSpace/Stalks.lean
theorem id (X : PresheafedSpace.{_, _, v} C) (x : X) :
    (𝟙 X : X ⟶ X).stalkMap x = 𝟙 (X.presheaf.stalk x)

Proof state:
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
e_1✝ :
  (X.presheaf.stalk x ⟶ X.presheaf.stalk x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)
⊢ (𝟙 X).c ≫ (Pushforward.id X.presheaf).hom = 𝟙 X.presheaf

Tactic:
ext

Result:
case h.e'_2.h.h.e'_8.w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
e_1✝ :
  (X.presheaf.stalk x ⟶ X.presheaf.stalk x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)
U✝ : Opens ↑↑X
⊢ ((𝟙 X).c ≫ (Pushforward.id X.presheaf).hom).app (op U✝) = (𝟙 X.presheaf).app (op U✝)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ Hom.stalkMap (𝟙 X) x = 𝟙 (X.presheaf.stalk x)

Tactic:
dsimp [Hom.stalkMap]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C x).map (𝟙 X).c ≫ stalkPushforward C (𝟙 ↑X) X.presheaf x = 𝟙 (X.presheaf.stalk x)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C x).map (𝟙 X).c ≫ stalkPushforward C (𝟙 ↑X) X.presheaf x = 𝟙 (X.presheaf.stalk x)

Tactic:
simp only [stalkPushforward.id]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C x).map (𝟙 X).c ≫ (stalkFunctor C x).map (Pushforward.id X.presheaf).hom = 𝟙 (X.presheaf.stalk x)

Proof state:
case h.e'_2.h.h.e'_8.w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
e_1✝ :
  (X.presheaf.stalk x ⟶ X.presheaf.stalk x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)
U✝ : Opens ↑↑X
⊢ 𝟙 (((pushforward C (𝟙 ↑X)).obj X.presheaf).obj (op U✝)) = (𝟙 X.presheaf).app (op U✝)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C x).map ((𝟙 X).c ≫ (Pushforward.id X.presheaf).hom) = 𝟙 (X.presheaf.stalk x)

Tactic:
convert (stalkFunctor C x).map_id X.presheaf

Result:
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
e_1✝ :
  (X.presheaf.stalk x ⟶ X.presheaf.stalk x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)
⊢ (𝟙 X).c ≫ (Pushforward.id X.presheaf).hom = 𝟙 X.presheaf

Proof state:
case h.e'_2.h.h.e'_8.w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
e_1✝ :
  (X.presheaf.stalk x ⟶ X.presheaf.stalk x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)
U✝ : Opens ↑↑X
⊢ ((𝟙 X).c ≫ (Pushforward.id X.presheaf).hom).app (op U✝) = (𝟙 X.presheaf).app (op U✝)

Tactic:
simp only [id_c, id_comp, Pushforward.id_hom_app, op_obj, eqToHom_refl, map_id]

Result:
case h.e'_2.h.h.e'_8.w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
e_1✝ :
  (X.presheaf.stalk x ⟶ X.presheaf.stalk x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)
U✝ : Opens ↑↑X
⊢ 𝟙 (((pushforward C (𝟙 ↑X)).obj X.presheaf).obj (op U✝)) = (𝟙 X.presheaf).app (op U✝)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C x).map (𝟙 X).c ≫ (stalkFunctor C x).map (Pushforward.id X.presheaf).hom = 𝟙 (X.presheaf.stalk x)

Tactic:
rw [← map_comp]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C x).map ((𝟙 X).c ≫ (Pushforward.id X.presheaf).hom) = 𝟙 (X.presheaf.stalk x)