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)
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op (PrimeSpectrum.basicOpen r)))
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
s : ↑S
n : ℕ
hsn :
  s' *
      (algebraMap ↑S ↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
        ↑(s, ⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 =
    (algebraMap ↑S ↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
      (s, ⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1
⊢ (CommRingCat.Hom.hom
          (CommRingCat.ofHom (algebraMap ↑R ↑S) ≫
            CommRingCat.ofHom
                (algebraMap (↑(CommRingCat.of ↑S))
                  ((structureSheafInType ↑(CommRingCat.of ↑S) ↑(CommRingCat.of ↑S)).obj.obj
                    ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).op.obj
                      (op ⊤)))) ≫
              ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                    (structureSheaf ↑(CommRingCat.of ↑S)).obj).germ
                ⊤ p trivial))
        ↑(s, ⟨r, hpr⟩ ^ n).2 *
      y =
    (toPushforwardStalkAlgHom R S p) (s, ⟨r, hpr⟩ ^ n).1

Tactic:
CommRingCat.comp_apply,

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)
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op (PrimeSpectrum.basicOpen r)))
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
s : ↑S
n : ℕ
hsn :
  s' *
      (algebraMap ↑S ↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
        ↑(s, ⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 =
    (algebraMap ↑S ↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
      (s, ⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1
⊢ (ConcreteCategory.hom
          (CommRingCat.ofHom
              (algebraMap (↑(CommRingCat.of ↑S))
                ((structureSheafInType ↑(CommRingCat.of ↑S) ↑(CommRingCat.of ↑S)).obj.obj
                  ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).op.obj (op ⊤)))) ≫
            ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                  (structureSheaf ↑(CommRingCat.of ↑S)).obj).germ
              ⊤ p trivial))
        ((ConcreteCategory.hom (CommRingCat.ofHom (algebraMap ↑R ↑S))) ↑(s, ⟨r, hpr⟩ ^ n).2) *
      y =
    (toPushforwardStalkAlgHom R S p) (s, ⟨r, hpr⟩ ^ n).1