-- Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
lemma of_specializingMap (H : (topologically @SpecializingMap).universally f) :
    ValuativeCriterion.Existence f

Proof state:
case mk.mk
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✝¹ : IsDomain ↑(CommRingCat.of R)
this✝ : ValuationRing ↑(CommRingCat.of R)
this : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
⊢ ⋯.HasLift

Tactic:
obtain ⟨x, h₁, h₂⟩ := @H (lft.base (closedPoint _)) _ (specializes_closedPoint (R := R) _)

Result:
case mk.mk.intro.intro
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✝¹ : IsDomain ↑(CommRingCat.of R)
this✝ : ValuationRing ↑(CommRingCat.of R)
this : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (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).toPresheafedSpace
h₁ : flip (fun x1 x2 => x1 ⤳ x2) x ((ConcreteCategory.hom lft.base) (closedPoint ↑(CommRingCat.of K)))
h₂ : (ConcreteCategory.hom (pullback.fst i₂ f).base) x = closedPoint R
⊢ ⋯.HasLift

Proof state:
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✝³ : IsDomain ↑(CommRingCat.of R)
this✝² : ValuationRing ↑(CommRingCat.of R)
this✝¹ : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (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).toPresheafedSpace
h₁ : flip (fun x1 x2 => x1 ⤳ x2) x ((ConcreteCategory.hom lft.base) (closedPoint ↑(CommRingCat.of K)))
h₂ : (ConcreteCategory.hom (pullback.fst i₂ f).base) x = closedPoint R
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((ConcreteCategory.hom (pullback.fst i₂ f).base) x) :=
  (stalkClosedPointIso (CommRingCat.of R)).symm ≪≫ (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✝ : IsLocalHom (CommRingCat.Hom.hom e.hom)
this : IsLocalHom (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
⊢ (Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫
      Scheme.Hom.app (pullback.fst i₂ f) ⊤ ≫
        Scheme.Hom.app lft ⊤ ≫
          (Functor.mapIso (Spec (CommRingCat.of K)).presheaf (eqToIso ⋯).op ≪≫ Scheme.ΓSpecIso (CommRingCat.of K)).hom =
    CommRingCat.ofHom (algebraMap R K)

Tactic:
erw [← Scheme.comp_app_assoc lft (pullback.fst i₂ f)]

Result:
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✝³ : IsDomain ↑(CommRingCat.of R)
this✝² : ValuationRing ↑(CommRingCat.of R)
this✝¹ : Field ↑(CommRingCat.of K) := field✝
H : topologically (@SpecializingMap) (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).toPresheafedSpace
h₁ : flip (fun x1 x2 => x1 ⤳ x2) x ((ConcreteCategory.hom lft.base) (closedPoint ↑(CommRingCat.of K)))
h₂ : (ConcreteCategory.hom (pullback.fst i₂ f).base) x = closedPoint R
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((ConcreteCategory.hom (pullback.fst i₂ f).base) x) :=
  (stalkClosedPointIso (CommRingCat.of R)).symm ≪≫ (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✝ : IsLocalHom (CommRingCat.Hom.hom e.hom)
this : IsLocalHom (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
⊢ (Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫
      Scheme.Hom.app (lft ≫ pullback.fst i₂ f) ⊤ ≫
        (Functor.mapIso (Spec (CommRingCat.of K)).presheaf (eqToIso ⋯).op ≪≫ Scheme.ΓSpecIso (CommRingCat.of K)).hom =
    CommRingCat.ofHom (algebraMap R K)

Proof state:
X Y : Scheme
f : X ⟶ Y
H : (topologically @SpecializingMap).universally f
⊢ Existence f

Tactic:
rintro ⟨R, K, i₁, i₂, ⟨w⟩⟩

Result:
case mk.mk
X Y : Scheme
f : X ⟶ Y
H : (topologically @SpecializingMap).universally f
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₂
⊢ ⋯.HasLift