-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
p : PrimeSpectrum (↑R : Type u)
inst : Algebra (↑R : Type u) (↑S : Type u)
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 (↑S : Type u)) : Type u)))
            (structureSheaf (↑S : Type u))))
        p) :
    Type u)
r : (↑(CommRingCat.of (↑R : Type u)) : Type u)
hpr :
  Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum (↑(CommRingCat.of (↑R : Type u)) : Type u)))
    (PrimeSpectrum.basicOpen r) p
s' :
  (↑(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 (PrimeSpectrum.basicOpen r))) :
    Type u)
e :
  (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 (PrimeSpectrum.basicOpen r)))
          (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 (↑S : Type u)) : Type u)))
                (structureSheaf (↑S : 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 (↑S : Type u)) : Type u)))
                (structureSheaf (↑S : Type u))))
            (PrimeSpectrum.basicOpen r) p hpr) :
        (a :
            (↑(((TopCat.Presheaf.pushforward CommRingCat
                          (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                      (structureSheaf (↑S : Type u)).obj).obj
                  (op (PrimeSpectrum.basicOpen r))) :
              Type u)) →
          (↑(((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))
      s' =
    y
s : (↑S : Type u)
n : ℕ
hsn :
  HMul.hMul (β :=
      (↑(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))
      s'
      ((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)))
                        (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) :
            (a : (↑S : Type u)) →
              (↑((structureSheaf (↑S : Type u)).obj.obj
                    (op
                      (PrimeSpectrum.basicOpen
                        ((algebraMap (↑R : Type u) (↑S : Type u) : (a : (↑R : Type u)) → (↑S : Type u)) r)))) :
                Type u))
          (↑(s,
                  Subtype.mk (p := fun (x : (↑S : Type u)) ↦
                    Membership.mem (γ := Submonoid (↑S : Type u))
                      (Submonoid.powers
                          ((algebraMap (↑R : Type u) (↑S : Type u) : (a : (↑R : Type u)) → (↑S : Type u)) r) :
                        Submonoid (↑S : Type u))
                      x)
                    ((fun (x : ℕ) ↦
                        HPow.hPow (α := (↑S : Type u))
                          ((algebraMap (↑R : Type u) (↑S : Type u) : (a : (↑R : Type u)) → (↑S : Type u)) r :
                            (↑S : Type u))
                          x)
                      n)
                    ⋯).2 :
            (↑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)))
                  (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)) =
    (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)))
                    (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) :
        (a : (↑S : Type u)) →
          (↑((structureSheaf (↑S : Type u)).obj.obj
                (op
                  (PrimeSpectrum.basicOpen
                    ((algebraMap (↑R : Type u) (↑S : Type u) : (a : (↑R : Type u)) → (↑S : Type u)) r)))) :
            Type u))
      (s,
          Subtype.mk (p := fun (x : (↑S : Type u)) ↦
            Membership.mem (γ := Submonoid (↑S : Type u))
              (Submonoid.powers ((algebraMap (↑R : Type u) (↑S : Type u) : (a : (↑R : Type u)) → (↑S : Type u)) r) :
                Submonoid (↑S : Type u))
              x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := (↑S : Type u))
                  ((algebraMap (↑R : Type u) (↑S : Type u) : (a : (↑R : Type u)) → (↑S : Type u)) r : (↑S : Type u)) x)
              n)
            ⋯).1
erw :
  HMul.hMul (α :=
      (↑(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 :=
              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 (PrimeSpectrum.basicOpen r)))
              (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 (↑S : Type u)) : Type u)))
                    (structureSheaf (↑S : 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 (↑S : Type u)) : Type u)))
                    (structureSheaf (↑S : Type u))))
                (PrimeSpectrum.basicOpen r) p hpr) :
            (a :
                (↑(((TopCat.Presheaf.pushforward CommRingCat
                              (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                          (structureSheaf (↑S : Type u)).obj).obj
                      (op (PrimeSpectrum.basicOpen r))) :
                  Type u)) →
              (↑(((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))
          ((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 ⊤))
                  (Y :=
                  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 (PrimeSpectrum.basicOpen r)))
                  (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))))
                    (Quiver.Hom.op (homOfLE ⋯))) :
                (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 (PrimeSpectrum.basicOpen r))) :
                    Type u))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X := CommRingCat.of (↑S : Type u)) (Y :=
                    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 R) : Type u))ᵒᵖ)
                          (Functor.op
                            (TopologicalSpace.Opens.map
                              (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))))
                          (op ⊤))))
                    (CommRingCat.ofHom
                      (algebraMap (↑(CommRingCat.of (↑S : Type u)) : Type u)
                        (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 R) : Type u))ᵒᵖ)
                            (Functor.op
                              (TopologicalSpace.Opens.map
                                (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))))
                            (op ⊤))))) :
                  (a : (↑(CommRingCat.of (↑S : Type u)) : Type u)) →
                    (↑(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))
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (X := R) (Y := CommRingCat.of (↑S : Type u))
                      (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))) :
                    (a : (↑R : Type u)) → (↑(CommRingCat.of (↑S : Type u)) : Type u))
                  (↑(s,
                          HPow.hPow (α := ↥p.asIdeal.primeCompl)
                            (Subtype.mk (p := fun (x : (↑R : Type u)) ↦ x ∈ p.asIdeal.primeCompl) r hpr) n).2 :
                    (↑R : Type u)))) :
            (↑(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 (PrimeSpectrum.basicOpen r))) :
              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))
      y =
    (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 (PrimeSpectrum.basicOpen r)))
          (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 (↑S : Type u)) : Type u)))
                (structureSheaf (↑S : 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 (↑S : Type u)) : Type u)))
                (structureSheaf (↑S : Type u))))
            (PrimeSpectrum.basicOpen r) p hpr) :
        (a :
            (↑(((TopCat.Presheaf.pushforward CommRingCat
                          (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                      (structureSheaf (↑S : Type u)).obj).obj
                  (op (PrimeSpectrum.basicOpen r))) :
              Type u)) →
          (↑(((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))
      ((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 ⊤))
              (Y :=
              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 (PrimeSpectrum.basicOpen r)))
              (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))))
                (Quiver.Hom.op (homOfLE ⋯))) :
            (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 (PrimeSpectrum.basicOpen r))) :
                Type u))
          ((CommRingCat.Hom.hom'
                (CommRingCat.ofHom
                  (algebraMap (↑(CommRingCat.of (↑S : Type u)) : Type u)
                    (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 ⊤))))) :
              (a : (↑(CommRingCat.of (↑S : Type u)) : Type u)) →
                (↑(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))
            (s,
                HPow.hPow (α := ↥p.asIdeal.primeCompl)
                  (Subtype.mk (p := fun (x : (↑R : Type u)) ↦ x ∈ p.asIdeal.primeCompl) r hpr) n).1) :
        (↑(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 (PrimeSpectrum.basicOpen r))) :
          Type u))
⊢ HMul.hMul (α :=
      (↑(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 :=
              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 (PrimeSpectrum.basicOpen r)))
              (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 (↑S : Type u)) : Type u)))
                    (structureSheaf (↑S : 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 (↑S : Type u)) : Type u)))
                    (structureSheaf (↑S : Type u))))
                (PrimeSpectrum.basicOpen r) p hpr) :
            (a :
                (↑(((TopCat.Presheaf.pushforward CommRingCat
                              (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                          (structureSheaf (↑S : Type u)).obj).obj
                      (op (PrimeSpectrum.basicOpen r))) :
                  Type u)) →
              (↑(((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))
          ((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 ⊤))
                  (Y :=
                  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 (PrimeSpectrum.basicOpen r)))
                  (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))))
                    (Quiver.Hom.op (homOfLE ⋯))) :
                (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 (PrimeSpectrum.basicOpen r))) :
                    Type u))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X := CommRingCat.of (↑S : Type u)) (Y :=
                    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 R) : Type u))ᵒᵖ)
                          (Functor.op
                            (TopologicalSpace.Opens.map
                              (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))))
                          (op ⊤))))
                    (CommRingCat.ofHom
                      (algebraMap (↑(CommRingCat.of (↑S : Type u)) : Type u)
                        (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 R) : Type u))ᵒᵖ)
                            (Functor.op
                              (TopologicalSpace.Opens.map
                                (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))))
                            (op ⊤))))) :
                  (a : (↑(CommRingCat.of (↑S : Type u)) : Type u)) →
                    (↑(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))
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (X := R) (Y := CommRingCat.of (↑S : Type u))
                      (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))) :
                    (a : (↑R : Type u)) → (↑(CommRingCat.of (↑S : Type u)) : Type u))
                  (↑(s,
                          HPow.hPow (α := ↥p.asIdeal.primeCompl)
                            (Subtype.mk (p := fun (x : (↑R : Type u)) ↦ x ∈ p.asIdeal.primeCompl) r hpr) n).2 :
                    (↑R : Type u)))) :
            (↑(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 (PrimeSpectrum.basicOpen r))) :
              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))
      y =
    (toPushforwardStalkAlgHom R S p :
        (a : (↑S : Type u)) →
          (↑(((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))
      (s,
          HPow.hPow (α := ↥p.asIdeal.primeCompl)
            (Subtype.mk (p := fun (x : (↑R : Type u)) ↦ x ∈ p.asIdeal.primeCompl) r hpr) n).1

Tactic:
erw [← (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).germ_res_apply
      (homOfLE le_top) p hpr]

Premises used: CommRingCat.carrier, Algebra.algebraMap, TopCat.Presheaf.germ_res_apply, CommRingCat.ofHom, AlgebraicGeometry.Spec.topMap, CategoryTheory.ObjectProperty.FullSubcategory.obj, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.Spec.structureSheaf, TopCat.Presheaf.pushforward, CategoryTheory.Functor.obj