-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (hypothesis)
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))
    ((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))
        x :
      (↑(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))
    (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 (↑S : Type u)) : Type u)))
                (structureSheaf (↑S : Type u))))
            p) :
        Type u))
⊢ ∃ (m : ↥p.asIdeal.primeCompl), m • x = 0
have 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))
  ((CommRingCat.Hom.hom
          (CategoryStruct.comp (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 (CommRingCat.of (↑R : Type u))) : 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 (CommRingCat.of (↑R : Type u))) : Type u))ᵒᵖ)
                    (Functor.op
                      (TopologicalSpace.Opens.map
                        (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))))
                    (op ⊤)))))
            (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)) :
        (a : (↑(CommRingCat.of (↑S : Type u)) : 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))
Tactic: rw [toPushforwardStalkAlgHom_apply,
      ← (toPushforwardStalk (CommRingCat.ofHom (algebraMap ↑R ↑S)) p).hom.map_zero,
      toPushforwardStalk] at hx
Cleared hypotheses: hx