-- 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
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
hbij :
  Function.Bijective (α := R) (β := ↥(CommRingCat.Hom.hom β).range)
    (⇑(RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) :
      (a : R) → ↥(CommRingCat.Hom.hom β).range)
φ : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of R :=
  CommRingCat.ofHom
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm
          (RingEquiv.ofBijective (RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) hbij)))
      (CommRingCat.Hom.hom β).rangeRestrict)
hαφ : α ≫ φ = 𝟙 (CommRingCat.of R)
hαφ' : Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.inv
hφβ : φ ≫ CommRingCat.ofHom (algebraMap R K) = β
refine_2 :
  CategoryStruct.comp (Y := Spec ((Spec (CommRingCat.of R)).presheaf.stalk (closedPoint R)))
      (Spec.map (Iso.hom (stalkClosedPointIso (CommRingCat.of R))))
      (Spec.map (Iso.inv (stalkClosedPointIso (CommRingCat.of R))) ≫ i₂) =
    i₂
refine_2₁ :
  Spec.map
        (CategoryStruct.comp (Y := (Spec (CommRingCat.of R)).presheaf.stalk (closedPoint R))
          (Iso.inv (stalkClosedPointIso (CommRingCat.of R))) (Iso.hom (stalkClosedPointIso (CommRingCat.of R)))) ≫
      i₂ =
    i₂
refine_2₂ : Spec.map (𝟙 (CommRingCat.of R)) ≫ i₂ = i₂
refine_2₃ : 𝟙 (Spec (CommRingCat.of R)) ≫ i₂ = i₂
refine_2₄ refine_2₅ : i₂ = i₂
⊢ CategoryStruct.comp (Y := Spec ((Spec (CommRingCat.of R)).presheaf.stalk (closedPoint R)))
      (Spec.map (Iso.hom (stalkClosedPointIso (CommRingCat.of R))))
      ((Spec (CommRingCat.of R)).fromSpecStalk (closedPoint R) ≫ i₂) =
    i₂

Tactic:
rw [← Spec_stalkClosedPointIso, ← Spec.map_comp_assoc,
      Iso.inv_hom_id, Spec.map_id, Category.id_comp]

Premises used: CategoryTheory.Iso.inv_hom_id, AlgebraicGeometry.Spec.map_id, AlgebraicGeometry.Spec.map_comp_assoc, AlgebraicGeometry.Spec_stalkClosedPointIso, CategoryTheory.Category.id_comp