-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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))
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 ⋯ :
        (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))) ⋯)))
    ((↑((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)
⊢ 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)

Tactic:
rw [comap_apply]

Premises used: AlgebraicGeometry.StructureSheaf.comap_apply