Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hp : p ∈ U
s :
  ToType
    (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op U))
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).map
            (homOfLE hrU).op))
        s) =
    y
s' : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
        (structureSheaf ↑S).obj).obj
    (op (PrimeSpectrum.basicOpen r))) :=
  (ConcreteCategory.hom
      (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
            (structureSheaf ↑S).obj).map
        (homOfLE hrU).op))
    s
h :
  s' =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).map
          (homOfLE hrU).op))
      s
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

Tactic:
replace e : ((Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).obj).germ _
      p hpr) s' = y := by
    rw [h]; exact e

Goal state after:
R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hp : p ∈ U
s :
  ToType
    (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op U))
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
s' : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
        (structureSheaf ↑S).obj).obj
    (op (PrimeSpectrum.basicOpen r))) :=
  (ConcreteCategory.hom
      (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
            (structureSheaf ↑S).obj).map
        (homOfLE hrU).op))
    s
h :
  s' =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).map
          (homOfLE hrU).op))
      s
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      s' =
    y
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1