-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑R : Type u)
inst : Algebra (↑R : Type u) (↑S : Type u)
x : (↑S : Type u)
hx :
  Eq (α :=
    (↑(TopCat.Presheaf.stalk
          (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
            (TopCat.Presheaf.pushforward CommRingCat
              (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
              (structureSheaf (↑S : Type u))))
          p) :
      Type u))
    (((CommRingCat.Hom.hom'
              (TopCat.Presheaf.germ
                (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                  (TopCat.Presheaf.pushforward CommRingCat
                    (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                  (ObjectProperty.FullSubcategory.obj (P :=
                    Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                    (structureSheaf (↑S : Type u))))
                ⊤ p trivial) :
            (↑(CommRingCat.of
                    (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
                      (ObjectProperty.FullSubcategory.obj (P :=
                        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                        (structureSheafInType (↑S : Type u) (↑S : Type u)))
                      (op
                        (Functor.obj (C := TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u)))
                          (TopologicalSpace.Opens.map
                            (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                          ⊤)))) :
                Type u) →+*
              (↑(TopCat.Presheaf.stalk
                    (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                      (TopCat.Presheaf.pushforward CommRingCat
                        (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                      (ObjectProperty.FullSubcategory.obj (P :=
                        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                        (structureSheaf (↑S : Type u))))
                    p) :
                Type u)) :
          (a :
              (structureSheafInType (↑S : Type u) (↑S : Type u)).obj.obj
                (op
                  ((TopologicalSpace.Opens.map
                        (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                    ⊤))) →
            (↑(((TopCat.Presheaf.pushforward CommRingCat
                          (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                      (structureSheaf (↑S : Type u)).obj).stalk
                  p) :
              Type u))
        ((CommRingCat.Hom.hom'
                (CommRingCat.ofHom
                  (algebraMap (↑S : Type u)
                    (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
                      (ObjectProperty.FullSubcategory.obj (P :=
                        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                        (structureSheafInType (↑S : Type u) (↑S : Type u)))
                      (op
                        (Functor.obj (C := TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u)))
                          (TopologicalSpace.Opens.map
                            (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                          ⊤))))) :
              (a : (↑S : Type u)) →
                (structureSheafInType (↑S : Type u) (↑S : Type u)).obj.obj
                  (op
                    ((TopologicalSpace.Opens.map
                          (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                      ⊤)))
            x :
          Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
              (structureSheafInType (↑S : Type u) (↑S : Type u)))
            (op
              (Functor.obj (C := TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u)))
                (TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                ⊤))) :
      (↑(TopCat.Presheaf.stalk
            (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
              (TopCat.Presheaf.pushforward CommRingCat
                (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                (structureSheaf (↑S : Type u))))
            p) :
        Type u))
    (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X :=
              CommRingCat.of
                (Functor.obj (C :=
                  (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑(CommRingCat.of (↑S : Type u)) : Type u)) : Type u))ᵒᵖ)
                  (ObjectProperty.FullSubcategory.obj (P :=
                    Presheaf.IsSheaf
                      (Opens.grothendieckTopology
                        (↑(PrimeSpectrum.Top (↑(CommRingCat.of (↑S : Type u)) : Type u)) : Type u)))
                    (structureSheafInType (↑(CommRingCat.of (↑S : Type u)) : Type u)
                      (↑(CommRingCat.of (↑S : Type u)) : Type u)))
                  (Functor.obj (C :=
                    (TopologicalSpace.Opens (↑(Spec.topObj (CommRingCat.of (↑R : Type u))) : Type u))ᵒᵖ)
                    (Functor.op
                      (TopologicalSpace.Opens.map
                        (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))))
                    (op ⊤))))
              (Y :=
              TopCat.Presheaf.stalk
                (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                  (TopCat.Presheaf.pushforward CommRingCat
                    (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                  (ObjectProperty.FullSubcategory.obj (P :=
                    Presheaf.IsSheaf
                      (Opens.grothendieckTopology
                        (↑(PrimeSpectrum.Top (↑(CommRingCat.of (↑S : Type u)) : Type u)) : Type u)))
                    (structureSheaf (↑(CommRingCat.of (↑S : Type u)) : Type u))))
                p)
              (TopCat.Presheaf.germ
                  (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                    (TopCat.Presheaf.pushforward CommRingCat
                      (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                    (ObjectProperty.FullSubcategory.obj (P :=
                      Presheaf.IsSheaf
                        (Opens.grothendieckTopology
                          (↑(PrimeSpectrum.Top (↑(CommRingCat.of (↑S : Type u)) : Type u)) : Type u)))
                      (structureSheaf (↑(CommRingCat.of (↑S : Type u)) : Type u))))
                  ⊤ p trivial :
                Functor.obj (C := (TopologicalSpace.Opens (↑(Spec.topObj (CommRingCat.of (↑R : Type u))) : Type u))ᵒᵖ)
                    (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                      (TopCat.Presheaf.pushforward CommRingCat
                        (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                      (ObjectProperty.FullSubcategory.obj (P :=
                        Presheaf.IsSheaf
                          (Opens.grothendieckTopology
                            (↑(PrimeSpectrum.Top (↑(CommRingCat.of (↑S : Type u)) : Type u)) : Type u)))
                        (structureSheaf (↑(CommRingCat.of (↑S : Type u)) : Type u))))
                    (op ⊤) ⟶
                  TopCat.Presheaf.stalk
                    (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                      (TopCat.Presheaf.pushforward CommRingCat
                        (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                      (ObjectProperty.FullSubcategory.obj (P :=
                        Presheaf.IsSheaf
                          (Opens.grothendieckTopology
                            (↑(PrimeSpectrum.Top (↑(CommRingCat.of (↑S : Type u)) : Type u)) : Type u)))
                        (structureSheaf (↑(CommRingCat.of (↑S : Type u)) : Type u))))
                    p) :
            (↑(CommRingCat.of
                    (Functor.obj (C :=
                      (TopologicalSpace.Opens
                          (↑(PrimeSpectrum.Top (↑(CommRingCat.of (↑S : Type u)) : Type u)) : Type u))ᵒᵖ)
                      (ObjectProperty.FullSubcategory.obj (P :=
                        Presheaf.IsSheaf
                          (Opens.grothendieckTopology
                            (↑(PrimeSpectrum.Top (↑(CommRingCat.of (↑S : Type u)) : Type u)) : Type u)))
                        (structureSheafInType (↑(CommRingCat.of (↑S : Type u)) : Type u)
                          (↑(CommRingCat.of (↑S : Type u)) : Type u)))
                      (Functor.obj (C :=
                        (TopologicalSpace.Opens (↑(Spec.topObj (CommRingCat.of (↑R : Type u))) : Type u))ᵒᵖ)
                        (Functor.op
                          (TopologicalSpace.Opens.map
                            (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))))
                        (op ⊤)))) :
                Type u) →+*
              (↑(TopCat.Presheaf.stalk
                    (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                      (TopCat.Presheaf.pushforward CommRingCat
                        (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                      (ObjectProperty.FullSubcategory.obj (P :=
                        Presheaf.IsSheaf
                          (Opens.grothendieckTopology
                            (↑(PrimeSpectrum.Top (↑(CommRingCat.of (↑S : Type u)) : Type u)) : Type u)))
                        (structureSheaf (↑(CommRingCat.of (↑S : Type u)) : Type u))))
                    p) :
                Type u)) :
          (a :
              (↑(CommRingCat.of
                    ((structureSheafInType (↑(CommRingCat.of (↑S : Type u)) : Type u)
                            (↑(CommRingCat.of (↑S : Type u)) : Type u)).obj.obj
                      ((TopologicalSpace.Opens.map
                              (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).op.obj
                        (op ⊤)))) :
                Type u)) →
            (↑(((TopCat.Presheaf.pushforward CommRingCat
                          (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                      (structureSheaf (↑(CommRingCat.of (↑S : Type u)) : Type u)).obj).stalk
                  p) :
              Type u))
        0 :
      (↑(TopCat.Presheaf.stalk
            (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
              (TopCat.Presheaf.pushforward CommRingCat
                (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology
                    (↑(PrimeSpectrum.Top (↑(CommRingCat.of (↑S : Type u)) : Type u)) : Type u)))
                (structureSheaf (↑(CommRingCat.of (↑S : Type u)) : Type u))))
            p) :
        Type u))
U : TopologicalSpace.Opens (↑(Spec.topObj (CommRingCat.of (↑R : Type u))) : Type u)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : (↑(CommRingCat.of (↑R : Type u)) : Type u)
hpr :
  Membership.mem (γ := Set (PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u)))
    ((fun (r : (↑(CommRingCat.of (↑R : Type u)) : Type u)) ↦
        (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u))))
      r)
    p
hrU :
  (fun (r : (↑(CommRingCat.of (↑R : Type u)) : Type u)) ↦
        (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u))))
      r ⊆
    U.carrier
e :
  Eq (α :=
    (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(Spec.topObj (CommRingCat.of (↑R : Type u))) : Type u))ᵒᵖ)
          (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
            (TopCat.Presheaf.pushforward CommRingCat
              (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
              (structureSheaf (↑S : Type u))))
          (op
            { carrier := {x : PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u) | r ∉ x.asIdeal},
              is_open' := ⋯ })) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            Functor.obj
              (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                (TopCat.Presheaf.pushforward CommRingCat
                  (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                  (structureSheaf (↑S : Type u))))
              (op U))
            (CategoryTheory.Functor.map
              (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                (TopCat.Presheaf.pushforward CommRingCat
                  (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                  (structureSheaf (↑S : Type u))))
              ((homOfLE (x :=
                    (fun (r : (↑(CommRingCat.of (↑R : Type u)) : Type u)) ↦
                        (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u))))
                      r)
                    (y := U.carrier) hrU).op
                (X :=
                (fun (r : (↑(CommRingCat.of (↑R : Type u)) : Type u)) ↦
                    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u))))
                  r)
                (Y := U.carrier))) :
          (a :
              (↑(((TopCat.Presheaf.pushforward CommRingCat
                            (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                        (structureSheaf (↑S : Type u)).obj).obj
                    (op U)) :
                Type u)) →
            (↑(((TopCat.Presheaf.pushforward CommRingCat
                          (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                      (structureSheaf (↑S : Type u)).obj).obj
                  (op
                    { carrier := {x : PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u) | r ∉ x.asIdeal},
                      is_open' := ⋯ })) :
              Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X :=
              Functor.obj (C := (TopologicalSpace.Opens (↑(Spec.topObj (CommRingCat.of (↑R : Type u))) : Type u))ᵒᵖ)
                (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                  (TopCat.Presheaf.pushforward CommRingCat
                    (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                  (ObjectProperty.FullSubcategory.obj (P :=
                    Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                    (structureSheaf (↑S : Type u))))
                (op ⊤))
              (CategoryTheory.Functor.map
                (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                  (TopCat.Presheaf.pushforward CommRingCat
                    (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                  (ObjectProperty.FullSubcategory.obj (P :=
                    Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                    (structureSheaf (↑S : Type u))))
                i₁.op) :
            (a :
                (↑(((TopCat.Presheaf.pushforward CommRingCat
                              (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                          (structureSheaf (↑S : Type u)).obj).obj
                      (op ⊤)) :
                  Type u)) →
              (↑(((TopCat.Presheaf.pushforward CommRingCat
                            (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                        (structureSheaf (↑S : Type u)).obj).obj
                    (op U)) :
                Type u))
          ((CommRingCat.Hom.hom'
                (CommRingCat.ofHom
                  (algebraMap (↑S : Type u)
                    (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
                      (ObjectProperty.FullSubcategory.obj (P :=
                        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                        (structureSheafInType (↑S : Type u) (↑S : Type u)))
                      (op
                        (Functor.obj (C := TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u)))
                          (TopologicalSpace.Opens.map
                            (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                          ⊤))))) :
              (a : (↑S : Type u)) →
                (structureSheafInType (↑S : Type u) (↑S : Type u)).obj.obj
                  (op
                    ((TopologicalSpace.Opens.map
                          (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                      ⊤)))
            x)) :
      (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(Spec.topObj (CommRingCat.of (↑R : Type u))) : Type u))ᵒᵖ)
            (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
              (TopCat.Presheaf.pushforward CommRingCat
                (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                (structureSheaf (↑S : Type u))))
            (op
              { carrier := {x : PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u) | r ∉ x.asIdeal},
                is_open' := ⋯ })) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            Functor.obj
              (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                (TopCat.Presheaf.pushforward CommRingCat
                  (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                  (structureSheaf (↑S : Type u))))
              (op U))
            (CategoryTheory.Functor.map
              (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                (TopCat.Presheaf.pushforward CommRingCat
                  (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                  (structureSheaf (↑S : Type u))))
              ((homOfLE (x :=
                    (fun (r : (↑(CommRingCat.of (↑R : Type u)) : Type u)) ↦
                        (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u))))
                      r)
                    (y := U.carrier) hrU).op
                (X :=
                (fun (r : (↑(CommRingCat.of (↑R : Type u)) : Type u)) ↦
                    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u))))
                  r)
                (Y := U.carrier))) :
          (a :
              (↑(((TopCat.Presheaf.pushforward CommRingCat
                            (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                        (structureSheaf (↑S : Type u)).obj).obj
                    (op U)) :
                Type u)) →
            (↑(((TopCat.Presheaf.pushforward CommRingCat
                          (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                      (structureSheaf (↑S : Type u)).obj).obj
                  (op
                    { carrier := {x : PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u) | r ∉ x.asIdeal},
                      is_open' := ⋯ })) :
              Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X :=
              Functor.obj (C := (TopologicalSpace.Opens (↑(Spec.topObj (CommRingCat.of (↑R : Type u))) : Type u))ᵒᵖ)
                (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                  (TopCat.Presheaf.pushforward CommRingCat
                    (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                  (ObjectProperty.FullSubcategory.obj (P :=
                    Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                    (structureSheaf (↑S : Type u))))
                (op ⊤))
              (CategoryTheory.Functor.map
                (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                  (TopCat.Presheaf.pushforward CommRingCat
                    (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                  (ObjectProperty.FullSubcategory.obj (P :=
                    Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                    (structureSheaf (↑S : Type u))))
                i₂.op) :
            (a :
                (↑(((TopCat.Presheaf.pushforward CommRingCat
                              (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                          (structureSheaf (↑S : Type u)).obj).obj
                      (op ⊤)) :
                  Type u)) →
              (↑(((TopCat.Presheaf.pushforward CommRingCat
                            (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                        (structureSheaf (↑S : Type u)).obj).obj
                    (op U)) :
                Type u))
          0) :
      (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(Spec.topObj (CommRingCat.of (↑R : Type u))) : Type u))ᵒᵖ)
            (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
              (TopCat.Presheaf.pushforward CommRingCat
                (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                (structureSheaf (↑S : Type u))))
            (op
              { carrier := {x : PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u) | r ∉ x.asIdeal},
                is_open' := ⋯ })) :
        Type u))
this :
  Eq (α :=
    (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
          (TopCat.Sheaf.presheaf (structureSheaf (↑S : Type u)))
          (Functor.obj (C := (TopologicalSpace.Opens (↑(Spec.topObj (CommRingCat.of (↑R : Type u))) : Type u))ᵒᵖ)
            (Functor.op
              (TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))))
            (op
              { carrier := {x : PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u) | r ∉ x.asIdeal},
                is_open' := ⋯ }))) :
      Type u))
    ((algebraMap (↑S : Type u)
            (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
                  (TopCat.Sheaf.presheaf (structureSheaf (↑S : Type u)))
                  (Functor.obj (C :=
                    (TopologicalSpace.Opens (↑(Spec.topObj (CommRingCat.of (↑R : Type u))) : Type u))ᵒᵖ)
                    (Functor.op
                      (TopologicalSpace.Opens.map
                        (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))))
                    (op
                      { carrier := {x : PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u) | r ∉ x.asIdeal},
                        is_open' := ⋯ }))) :
              Type u) :
          (a : (↑S : Type u)) →
            (↑((structureSheaf (↑S : Type u)).presheaf.obj
                  ((TopologicalSpace.Opens.map
                          (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).op.obj
                    (op
                      { carrier := {x : PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u) | r ∉ x.asIdeal},
                        is_open' := ⋯ }))) :
              Type u))
        x :
      (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
            (TopCat.Sheaf.presheaf (structureSheaf (↑S : Type u)))
            (Functor.obj (C := (TopologicalSpace.Opens (↑(Spec.topObj (CommRingCat.of (↑R : Type u))) : Type u))ᵒᵖ)
              (Functor.op
                (TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))))
              (op
                { carrier := {x : PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u) | r ∉ x.asIdeal},
                  is_open' := ⋯ }))) :
        Type u))
    (0 :
      (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
            (TopCat.Sheaf.presheaf (structureSheaf (↑S : Type u)))
            (Functor.obj (C := (TopologicalSpace.Opens (↑(Spec.topObj (CommRingCat.of (↑R : Type u))) : Type u))ᵒᵖ)
              (Functor.op
                (TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))))
              (op
                { carrier := {x : PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u) | r ∉ x.asIdeal},
                  is_open' := ⋯ }))) :
        Type u))
⊢ Eq (α :=
    (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
              (structureSheaf (↑S : Type u)) :
            (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ ⥤ CommRingCat)
          (op
              (PrimeSpectrum.basicOpen
                ((algebraMap (↑R : Type u) (↑S : Type u) : (a : (↑R : Type u)) → (↑S : Type u)) r)) :
            (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)) :
      Type u))
    (IsLocalization.mk' (M :=
      Submonoid.powers ((algebraMap (↑R : Type u) (↑S : Type u) : (a : (↑R : Type u)) → (↑S : Type u)) r))
      (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                (structureSheaf (↑S : Type u)) :
              (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ ⥤ CommRingCat)
            (op
                (PrimeSpectrum.basicOpen
                  ((algebraMap (↑R : Type u) (↑S : Type u) : (a : (↑R : Type u)) → (↑S : Type u)) r)) :
              (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)) :
        Type u)
      x 1)
    0

Tactic:
have :=
      (@IsLocalization.mk'_one _ _ _ _ _ _
            (StructureSheaf.IsLocalization.to_basicOpen S <| algebraMap R S r) x).trans
        this