-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u
inst_1 : CommRing S
f : R →+* S
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
x_1 : (↑(CommRingCat.of R) : Type u)
x :
  ↥(unop
        (op
          ((Opens.comap
                { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ : C(PrimeSpectrum S, PrimeSpectrum R) } :
              (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
            U)) :
      Opens (↑(PrimeSpectrum.Top S) : Type u))
⊢ Eq.{u + 1} (α := Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    ((↑((CommRingCat.Hom.hom
                (CommRingCat.ofHom
                    (algebraMap R
                      (↑(Functor.obj
                            (ObjectProperty.FullSubcategory.obj (P :=
                              CategoryTheory.Presheaf.IsSheaf
                                (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                              (structureSheaf R))
                            (op U)) :
                        Type u)) ≫
                  CommRingCat.ofHom
                    (comap f U
                      ((Opens.comap
                            { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ :
                              C(PrimeSpectrum S, PrimeSpectrum R) } :
                          (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                        U)
                      ⋯)) :
              (a : (↑(CommRingCat.of R) : Type u)) →
                (↑(CommRingCat.of
                      (↑((structureSheaf S).obj.obj
                            (op
                              ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ } :
                                  (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                                U))) :
                        Type u)) :
                  Type u))
            x_1) :
        (x :
            ↥(unop
                (op
                  ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ } :
                      (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                    U)))) →
          Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      x)
    ((↑((CommRingCat.Hom.hom
                (CommRingCat.ofHom f ≫
                  CommRingCat.ofHom
                    (algebraMap S
                      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top S) : Type u))ᵒᵖ)
                            (ObjectProperty.FullSubcategory.obj (P :=
                              CategoryTheory.Presheaf.IsSheaf
                                (Opens.grothendieckTopology (↑(PrimeSpectrum.Top S) : Type u)))
                              (structureSheaf S))
                            (op
                              ((Opens.comap
                                    { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ :
                                      C(PrimeSpectrum S, PrimeSpectrum R) } :
                                  (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                                U))) :
                        Type u))) :
              (a : (↑(CommRingCat.of R) : Type u)) →
                (↑(CommRingCat.of
                      (↑((structureSheaf S).obj.obj
                            (op
                              ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ } :
                                  (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                                U))) :
                        Type u)) :
                  Type u))
            x_1) :
        (x :
            ↥(unop
                (op
                  ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ } :
                      (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                    U)))) →
          Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      x)
have dsimp : Eq.{u + 1} (α := Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
  ((↑((comap f U
              ((Opens.comap
                    { toFun := PrimeSpectrum.comap f, continuous_toFun := sorry : C(PrimeSpectrum S, PrimeSpectrum R) } :
                  (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                U)
              sorry :
            (a : (↑((structureSheaf R).obj.obj (op U)) : Type u)) →
              (↑((structureSheaf S).obj.obj
                    (op
                      ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := sorry } :
                          (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                        U))) :
                Type u))
          ((algebraMap R
                (↑(Functor.obj
                      (ObjectProperty.FullSubcategory.obj (P :=
                        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                        (structureSheaf R))
                      (op U)) :
                  Type u) :
              (a : R) → (↑((structureSheaf R).obj.obj (op U)) : Type u))
            x_1)) :
      (x :
          ↥((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := sorry } :
                (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
              U)) →
        Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    x)
  ((↑((algebraMap S
              (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top S) : Type u))ᵒᵖ)
                    (ObjectProperty.FullSubcategory.obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top S) : Type u)))
                      (structureSheaf S))
                    (op
                      ((Opens.comap
                            { toFun := PrimeSpectrum.comap f, continuous_toFun := sorry :
                              C(PrimeSpectrum S, PrimeSpectrum R) } :
                          (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                        U))) :
                Type u) :
            (a : S) →
              (↑((structureSheaf S).obj.obj
                    (op
                      ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := sorry } :
                          (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                        U))) :
                Type u))
          ((f : (a : R) → S) x_1)) :
      (x :
          ↥((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := sorry } :
                (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
              U)) →
        Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    x)
Tactic: dsimp