-- Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
@[stacks 01KE]
lemma specializingMap (H : ValuativeCriterion.Existence f) :
    SpecializingMap f.base

Proof state:
case intro.intro.intro.mk.refine_1
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : flip (fun x1 x2 => x1 ⤳ x2) y ((ConcreteCategory.hom f.base) x')
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring ↑(X.residueField x')
hA : ∀ (x : ↑(Y.presheaf.stalk y)), (CommRingCat.Hom.hom stalk_y_to_residue_x') x ∈ A.toSubring
hA_local : IsLocalHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
w :
  X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
l :
  Spec
      (CommRingCat.of
        (ValuativeCommSq.mk (↥A) (↑(X.residueField x')) (X.fromSpecResidueField x')
            (Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y) ⋯).R) ⟶
    X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ l = X.fromSpecResidueField x'
hl₂ : l ≫ f = Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
⊢ flip (fun x1 x2 => x1 ⤳ x2) ((ConcreteCategory.hom l.base) (closedPoint ↥A)) x'

Tactic:
simp_rw [← Scheme.fromSpecResidueField_apply x' (closedPoint (X.residueField x')), ← hl₁]

Result:
case intro.intro.intro.mk.refine_1
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : flip (fun x1 x2 => x1 ⤳ x2) y ((ConcreteCategory.hom f.base) x')
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring ↑(X.residueField x')
hA : ∀ (x : ↑(Y.presheaf.stalk y)), (CommRingCat.Hom.hom stalk_y_to_residue_x') x ∈ A.toSubring
hA_local : IsLocalHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
w :
  X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
l :
  Spec
      (CommRingCat.of
        (ValuativeCommSq.mk (↥A) (↑(X.residueField x')) (X.fromSpecResidueField x')
            (Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y) ⋯).R) ⟶
    X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ l = X.fromSpecResidueField x'
hl₂ : l ≫ f = Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
⊢ flip (fun x1 x2 => x1 ⤳ x2) ((ConcreteCategory.hom l.base) (closedPoint ↥A))
    ((ConcreteCategory.hom (Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ l).base)
      (closedPoint ↑(X.residueField x')))

Proof state:
X Y : Scheme
f : X ⟶ Y
H : Existence f
⊢ SpecializingMap ⇑(ConcreteCategory.hom f.base)

Tactic:
intro x' y h

Result:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : flip (fun x1 x2 => x1 ⤳ x2) y ((ConcreteCategory.hom f.base) x')
⊢ ∃ a', flip (fun x1 x2 => x1 ⤳ x2) a' x' ∧ (ConcreteCategory.hom f.base) a' = y

Proof state:
case intro.intro.intro.mk.refine_2
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : flip (fun x1 x2 => x1 ⤳ x2) y ((ConcreteCategory.hom f.base) x')
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring ↑(X.residueField x')
hA : ∀ (x : ↑(Y.presheaf.stalk y)), (CommRingCat.Hom.hom stalk_y_to_residue_x') x ∈ A.toSubring
hA_local : IsLocalHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
w :
  X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
l :
  Spec
      (CommRingCat.of
        (ValuativeCommSq.mk (↥A) (↑(X.residueField x')) (X.fromSpecResidueField x')
            (Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y) ⋯).R) ⟶
    X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ l = X.fromSpecResidueField x'
hl₂ : l ≫ f = Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
⊢ (ConcreteCategory.hom (Y.fromSpecStalk y).base)
      ((ConcreteCategory.hom (Spec.map stalk_y_to_A).base) (closedPoint ↥A)) =
    y

Tactic:
have : (Spec.map stalk_y_to_A).base (closedPoint A) = closedPoint (Y.presheaf.stalk y) :=
  comap_closedPoint (S := A) (stalk_y_to_residue_x'.hom.codRestrict A.toSubring hA)

Result:
case intro.intro.intro.mk.refine_2
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : flip (fun x1 x2 => x1 ⤳ x2) y ((ConcreteCategory.hom f.base) x')
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring ↑(X.residueField x')
hA : ∀ (x : ↑(Y.presheaf.stalk y)), (CommRingCat.Hom.hom stalk_y_to_residue_x') x ∈ A.toSubring
hA_local : IsLocalHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
w :
  X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
l :
  Spec
      (CommRingCat.of
        (ValuativeCommSq.mk (↥A) (↑(X.residueField x')) (X.fromSpecResidueField x')
            (Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y) ⋯).R) ⟶
    X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ l = X.fromSpecResidueField x'
hl₂ : l ≫ f = Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
this : (ConcreteCategory.hom (Spec.map stalk_y_to_A).base) (closedPoint ↥A) = closedPoint ↑(Y.presheaf.stalk y)
⊢ (ConcreteCategory.hom (Y.fromSpecStalk y).base)
      ((ConcreteCategory.hom (Spec.map stalk_y_to_A).base) (closedPoint ↥A)) =
    y

Proof state:
case intro.intro
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : flip (fun x1 x2 => x1 ⤳ x2) y ((ConcreteCategory.hom f.base) x')
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring ↑(X.residueField x')
hA : ∀ (x : ↑(Y.presheaf.stalk y)), (CommRingCat.Hom.hom stalk_y_to_residue_x') x ∈ A.toSubring
hA_local : IsLocalHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
⊢ ∃ a', flip (fun x1 x2 => x1 ⤳ x2) a' x' ∧ (ConcreteCategory.hom f.base) a' = y

Tactic:
let stalk_y_to_A : Y.presheaf.stalk y ⟶ .of A :=
  CommRingCat.ofHom (stalk_y_to_residue_x'.hom.codRestrict _ hA)

Result:
case intro.intro
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : flip (fun x1 x2 => x1 ⤳ x2) y ((ConcreteCategory.hom f.base) x')
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring ↑(X.residueField x')
hA : ∀ (x : ↑(Y.presheaf.stalk y)), (CommRingCat.Hom.hom stalk_y_to_residue_x') x ∈ A.toSubring
hA_local : IsLocalHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
⊢ ∃ a', flip (fun x1 x2 => x1 ⤳ x2) a' x' ∧ (ConcreteCategory.hom f.base) a' = y