-- 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)))
    ((↑((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 : (↑((structureSheaf R).obj.obj (op U)) : Type u)) →
                (↑((structureSheaf S).obj.obj
                      (op
                        ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ } :
                            (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 := ⋯ } :
                  (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 := ⋯ :
                                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 := ⋯ } :
                            (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 := ⋯ } :
                  (a : Opens (PrimeSpectrum R)) → Opens (PrimeSpectrum S))
                U)) →
          Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      x)
have rw : Eq (α := Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
  ((Localization.localRingHom (PrimeSpectrum.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal
        (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f sorry :
      (a : Localization.AtPrime (PrimeSpectrum.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal) →
        Localization.AtPrime (↑x : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
    ((↑((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 : ↥(unop (op U))) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
      (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U))
        (PrimeSpectrum.comap f (↑x : (↑(PrimeSpectrum.Top S) : Type u))) sorry)))
  ((↑((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: rw [comap_apply]