-- 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
change :
  Iso.inv (Scheme.ΓSpecIso (CommRingCat.of R)) ≫
      (Spec (CommRingCat.of R)).presheaf.germ ⊤ (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)
⊢ 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))

Tactic:
change (Scheme.ΓSpecIso (.of R)).inv ≫ (Spec <| .of R).presheaf.germ _ _ _ ≫ _ = _

Premises used: AlgebraicGeometry.Spec, AlgebraicGeometry.Scheme.ΓSpecIso, TopCat.Presheaf.germ, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CommRingCat.of, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Iso.inv, AlgebraicGeometry.Scheme.toLocallyRingedSpace