-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this_4 :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
simp :
  Eq (α := CommRingCat.of R ⟶ CommRingCat.of K)
    (CategoryStruct.comp (Y :=
      CommRingCat.of
        (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u))) (structureSheafInType R R))
          (Opposite.op ⊤)))
      (CommRingCat.ofHom
        (algebraMap R
          (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R R))
            (Opposite.op ⊤))))
      (TopCat.Presheaf.germ (structurePresheafInCommRingCat R) ⊤ (closedPoint R) trivial ≫
        (Spec (CommRingCat.of R)).presheaf.stalkSpecializes ⋯ ≫
          Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫
            (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft))
    (CommRingCat.ofHom (algebraMap R K))
⊢ α ≫ β = CommRingCat.ofHom (algebraMap R K)

Tactic:
simp only [CommRingCat.coe_of, Iso.trans_hom, Iso.symm_hom, TopCat.Presheaf.stalkCongr_hom,
      Category.assoc, α, e, β, stalkClosedPointIso_inv, StructureSheaf.toStalk]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.symm_hom, TopCat.Presheaf.stalkCongr_hom, CommRingCat.coe_of, CategoryTheory.Iso.trans_hom, AlgebraicGeometry.stalkClosedPointIso_inv, AlgebraicGeometry.StructureSheaf.toStalk