-- 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))
          (HPow.hPow (α := (↑S : Type u))
            ((algebraMap (↑R : Type u) (↑S : Type u) : (a : (↑R : Type u)) → (↑S : Type u)) r : (↑S : Type u)) n) :
        (↑(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
f : 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)) ⟶
  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
⊢ 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))
          ((algebraMap (↑R : Type u) (↑S : Type u) : (a : (↑R : Type u)) → (↑S : Type u)) (r ^ n)) :
        (↑(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

Tactic:
rw [← map_pow (algebraMap R S)] at hsn

Premises used: CommRingCat.carrier, Algebra.algebraMap, map_pow