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

Proof state:
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
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
⊢ ⋯.HasLift

Tactic:
have : IsLocalHom e.hom.hom := isLocalHom_of_isIso e.hom

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
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)
⊢ ⋯.HasLift

Proof state:
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

Tactic:
let e : CommRingCat.of R ≅ (Spec (.of R)).presheaf.stalk ((pullback.fst i₂ f).base x) :=
  (stalkClosedPointIso (.of R)).symm ≪≫
    (Spec (.of R)).presheaf.stalkCongr (.of_eq h₂.symm)

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
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 ⋯
⊢ ⋯.HasLift