-- 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_1 :
  Y.presheaf.stalk (f x) ≅
    CommRingCat.of (Localization.AtPrime (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal)
refine_2 :
  X.presheaf.stalk x ≅
    CommRingCat.of (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal)
refine_3 :
  Eq (α :=
    Y.presheaf.stalk (f x) ⟶
      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)) ⋯)))
    (Scheme.Hom.stalkMap f x ≫
      Iso.hom
        (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)))))
⊢ Arrow.mk (Scheme.Hom.stalkMap f x) ≅
    Arrow.mk (X :=
      CommRingCat.of (Localization.AtPrime (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal))
      (Y :=
      CommRingCat.of (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).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)) ⋯))

Tactic:
refine Arrow.isoMk' _ _ ?_ ?_ ?_

Premises used: CategoryTheory.Arrow.isoMk'