-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
U_1 : X.Opens
hU_1 : IsAffineOpen U_1
f_1 : (↑Γ(X, U_1) : Type u)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this_1 : Algebra (↑(Y.presheaf.obj (op U)) : Type u)
  (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u) :=
  Y.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)
this_2 :
  IsLocalization.AtPrime (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
this_3 : Algebra (↑(X.presheaf.obj (op V)) : Type u)
  (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u) :=
  X.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)
this :
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u)
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
refine_3 :
  Eq (α := (↑Γ(Y, U) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (RingHom.comp (β := (↑(Y.presheaf.stalk (f x)) : Type u))
      (CommRingCat.Hom.hom
        (CategoryStruct.comp (Y :=
          CommRingCat.of (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal))
          (CategoryStruct.comp (Y :=
            CommRingCat.of
              (Localization.AtPrime (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal))
            (Iso.hom
              (RingEquiv.toCommRingCatIso
                (AlgEquiv.toRingEquiv
                  (IsLocalization.algEquiv
                    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal.primeCompl
                    (↑(Y.presheaf.stalk (f x)) : Type u)
                    (Localization.AtPrime
                      (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal)))))
            (CommRingCat.ofHom
              (Localization.localRingHom (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
                (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
                (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯)))
          (Iso.inv
            (RingEquiv.toCommRingCatIso
              (AlgEquiv.toRingEquiv
                (IsLocalization.algEquiv
                  (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal.primeCompl
                  (↑(X.presheaf.stalk x) : Type u)
                  (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal)))))))
      (algebraMap (↑Γ(Y, U) : Type u) (↑(Y.presheaf.stalk (f x)) : Type u)))
    ((CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).comp
      (algebraMap (↑Γ(Y, U) : Type u) (↑(Y.presheaf.stalk (f x)) : Type u)))
⊢ CommRingCat.Hom.hom
      (CategoryStruct.comp (Y :=
        CommRingCat.of (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal))
        (CategoryStruct.comp (Y :=
          CommRingCat.of
            (Localization.AtPrime (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal))
          (Iso.hom
            (RingEquiv.toCommRingCatIso
              (AlgEquiv.toRingEquiv
                (IsLocalization.algEquiv
                  (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal.primeCompl
                  (↑(Y.presheaf.stalk (f x)) : Type u)
                  (Localization.AtPrime (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal)))))
          (CommRingCat.ofHom
            (Localization.localRingHom (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
              (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯)))
        (Iso.inv
          (RingEquiv.toCommRingCatIso
            (AlgEquiv.toRingEquiv
              (IsLocalization.algEquiv
                (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal.primeCompl
                (↑(X.presheaf.stalk x) : Type u)
                (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal)))))) =
    CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)

Tactic:
apply IsLocalization.ringHom_ext
      (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal.primeCompl

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Subtype.mk, AlgebraicGeometry.IsAffineOpen.primeIdealOf, AlgebraicGeometry.PresheafedSpace.Hom.base, Ideal.primeCompl, DFunLike.coe, PrimeSpectrum.asIdeal, IsLocalization.ringHom_ext