-- 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 (α :=
    (↑(((TopologicalSpace.Opens.map (InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R))).base).op ⋙
              (sheafedSpaceObj R).presheaf).obj
          (op U)) :
      Type u))
    ((CommRingCat.Hom.hom
            (NatTrans.app
              ((sheafedSpaceMap (𝟙 R)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj R).presheaf) (op U)) :
          (a : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)) →
            (↑(((TopologicalSpace.Opens.map (𝟙 (sheafedSpaceObj R)).hom.base).op ⋙ (sheafedSpaceObj R).presheaf).obj
                  (op U)) :
              Type u))
        x :
      (↑(((TopologicalSpace.Opens.map (InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R))).base).op ⋙
                (sheafedSpaceObj R).presheaf).obj
            (op U)) :
        Type u))
    ((CommRingCat.Hom.hom ((InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R))).c.app (op U)) :
          (a : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)) →
            (↑(((TopologicalSpace.Opens.map (𝟙 (sheafedSpaceObj R)).hom.base).op ⋙ (sheafedSpaceObj R).presheaf).obj
                  (op U)) :
              Type u))
        x :
      (↑(((TopologicalSpace.Opens.map (InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R))).base).op ⋙
                (sheafedSpaceObj R).presheaf).obj
            (op 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))
      ((comap (RingHom.id (↑R : Type u)) U ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U) 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: dsimp