-- Mathlib/AlgebraicGeometry/Spec.lean
theorem Spec.sheafedSpaceMap_id {R : CommRingCat.{u}} :
    Spec.sheafedSpaceMap (𝟙 R) = 𝟙 (Spec.sheafedSpaceObj R) :=
  AlgebraicGeometry.PresheafedSpace.Hom.ext _ _ (Spec.topMap_id R) <| by
    ext
    dsimp
    rw [comap_id (by simp)]
    simp
    rfl

Proof state:
case w.hf.a
R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom ((structureSheaf ↑R).val.map (𝟙 (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝)))))
      ((comap (RingHom.id ↑R) U✝ ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝) ⋯) x✝) =
    (RingHom.id ↑((structureSheaf ↑R).val.obj (op U✝))) x✝

Tactic:
rw [comap_id (by simp)]

Result:
case w.hf.a
R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom ((structureSheaf ↑R).val.map (𝟙 (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝)))))
      ((CommRingCat.Hom.hom (eqToHom ⋯)) x✝) =
    (RingHom.id ↑((structureSheaf ↑R).val.obj (op U✝))) x✝

Proof state:
R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ U✝ = (TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝

Tactic:
simp

Result:
no goals

Proof state:
case w.hf.a
R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (RingHom.id ↑((structureSheaf ↑R).val.obj (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝)))) x✝ =
    (RingHom.id ↑((structureSheaf ↑R).val.obj (op U✝))) x✝

Tactic:
rfl

Result:
no goals

Proof state:
case w.hf.a
R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (((sheafedSpaceMap (𝟙 R)).c ≫ whiskerRight (eqToHom ⋯) (sheafedSpaceObj R).presheaf).app (op U✝)))
      x✝ =
    (CommRingCat.Hom.hom ((𝟙 (sheafedSpaceObj R)).c.app (op U✝))) x✝

Tactic:
dsimp

Result:
case w.hf.a
R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom ((structureSheaf ↑R).val.map (𝟙 (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝)))))
      ((comap (RingHom.id ↑R) U✝ ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝) ⋯) x✝) =
    (RingHom.id ↑((structureSheaf ↑R).val.obj (op U✝))) x✝

Proof state:
R : CommRingCat
⊢ (sheafedSpaceMap (𝟙 R)).c ≫ whiskerRight (eqToHom ⋯) (sheafedSpaceObj R).presheaf = (𝟙 (sheafedSpaceObj R)).c

Tactic:
ext

Result:
case w.hf.a
R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (((sheafedSpaceMap (𝟙 R)).c ≫ whiskerRight (eqToHom ⋯) (sheafedSpaceObj R).presheaf).app (op U✝)))
      x✝ =
    (CommRingCat.Hom.hom ((𝟙 (sheafedSpaceObj R)).c.app (op U✝))) x✝

Proof state:
case w.hf.a
R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom ((structureSheaf ↑R).val.map (𝟙 (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝)))))
      ((CommRingCat.Hom.hom (eqToHom ⋯)) x✝) =
    (RingHom.id ↑((structureSheaf ↑R).val.obj (op U✝))) x✝

Tactic:
simp

Result:
case w.hf.a
R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (RingHom.id ↑((structureSheaf ↑R).val.obj (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝)))) x✝ =
    (RingHom.id ↑((structureSheaf ↑R).val.obj (op U✝))) x✝