-- 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))
dsimp :
  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)
⊢ 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)

Tactic:
dsimp