-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
U : TopologicalSpace.Opens (↑(↑(sheafedSpaceObj R).toPresheafedSpace : TopCat) : Type u)
x : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)
h :
  Eq (α :=
    (↑(Functor.obj
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
            (structureSheaf (↑R : Type u)))
          (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
      Type u))
    ((CommRingCat.Hom.hom
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (structureSheaf (↑R : Type u)))
              (𝟙 (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U)))) :
          (a :
              (↑((structureSheaf (↑R : Type u)).obj.obj (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
                Type u)) →
            (↑((structureSheaf (↑R : Type u)).obj.obj (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
              Type u))
        ((CommRingCat.Hom.hom (eqToHom ⋯) :
            (a : (↑((structureSheaf (↑R : Type u)).obj.obj (op U)) : Type u)) →
              (↑((structureSheaf (↑R : Type u)).obj.obj (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
                Type u))
          x) :
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheaf (↑R : Type u)))
            (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
        Type u))
    ((CommRingCat.Hom.hom ((PresheafedSpace.Hom.c (𝟙 (sheafedSpaceObj R).toPresheafedSpace)).app (op U)) :
          (a : (↑((structureSheaf (↑R : Type u)).obj.obj (op U)) : Type u)) →
            (↑((structureSheaf (↑R : Type u)).obj.obj (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
              Type u))
        x :
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheaf (↑R : Type u)))
            (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
        Type u))
⊢ Eq (α :=
    (↑(Functor.obj
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
            (structureSheaf (↑R : Type u)))
          (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
      Type u))
    ((CommRingCat.Hom.hom
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (structureSheaf (↑R : Type u)))
              (𝟙 (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U)))) :
          (a :
              (↑((structureSheaf (↑R : Type u)).obj.obj (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
                Type u)) →
            (↑((structureSheaf (↑R : Type u)).obj.obj (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
              Type u))
        ((comap (RingHom.id (↑R : Type u)) U ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U) ⋯ :
            (a : (↑((structureSheaf (↑R : Type u)).obj.obj (op U)) : Type u)) →
              (↑((structureSheaf (↑R : Type u)).obj.obj (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
                Type u))
          x) :
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheaf (↑R : Type u)))
            (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
        Type u))
    ((CommRingCat.Hom.hom ((PresheafedSpace.Hom.c (𝟙 (sheafedSpaceObj R).toPresheafedSpace)).app (op U)) :
          (a : (↑((structureSheaf (↑R : Type u)).obj.obj (op U)) : Type u)) →
            (↑((structureSheaf (↑R : Type u)).obj.obj (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
              Type u))
        x :
      (↑(Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheaf (↑R : Type u)))
            (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U))) :
        Type u))

Tactic:
rw [comap_id (by simp)]

Premises used: AlgebraicGeometry.StructureSheaf.comap_id