-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R : CommRingCat
U : TopologicalSpace.Opens (↑(↑(sheafedSpaceObj R).toPresheafedSpace : TopCat) : Type u)
x : (↑((sheafedSpaceObj R).presheaf.obj (op 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))
have 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 sorry) :
          (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)]