-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (α := ↥Y) (fun (x1 x2 : ↥Y) ↦ x1 ⤳ x2) y (f x' : ↥Y)
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') : Type u)
hA :
  ∀ (x : (↑(Y.presheaf.stalk y) : Type u)),
    Membership.mem (α := (↑(X.residueField x') : Type u)) A.toSubring
      ((CommRingCat.Hom.hom stalk_y_to_residue_x' :
            (a : (↑(Y.presheaf.stalk y) : Type u)) → (↑(X.residueField x') : Type u))
          x :
        (↑(X.residueField x') : Type u))
hA_local :
  IsLocalHom (R := (↑(Y.presheaf.stalk y) : Type u)) (S := ↥A.toSubring) (F :=
    (↑(Y.presheaf.stalk y) : Type u) →+* ↥A.toSubring)
    ((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') : Type u))) ≫
      Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
obtain :
  ∀
    (l :
      Spec
          (CommRingCat.of
            { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := ⋯, valuationRing := ⋯,
                K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
                algebra := A.instAlgebraSubtypeMem, isFractionRing := ⋯, i₁ := X.fromSpecResidueField x',
                i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := ⋯ : ValuativeCommSq f }.R) ⟶
        X)
    (hl₁ :
      Spec.map
            (CommRingCat.ofHom
              (algebraMap
                { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := ⋯, valuationRing := ⋯,
                    K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
                    algebra := A.instAlgebraSubtypeMem, isFractionRing := ⋯, i₁ := X.fromSpecResidueField x',
                    i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := ⋯ : ValuativeCommSq f }.R
                { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := ⋯, valuationRing := ⋯,
                    K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
                    algebra := A.instAlgebraSubtypeMem, isFractionRing := ⋯, i₁ := X.fromSpecResidueField x',
                    i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := ⋯ : ValuativeCommSq f }.K)) ≫
          l =
        { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := ⋯, valuationRing := ⋯,
            K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
            algebra := A.instAlgebraSubtypeMem, isFractionRing := ⋯, i₁ := X.fromSpecResidueField x',
            i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := ⋯ : ValuativeCommSq f }.i₁)
    (hl₂ :
      l ≫ f =
        { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := ⋯, valuationRing := ⋯,
            K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
            algebra := A.instAlgebraSubtypeMem, isFractionRing := ⋯, i₁ := X.fromSpecResidueField x',
            i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := ⋯ }.i₂),
    ∃ (a' : ↥X), flip (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) a' x' ∧ f a' = y
⊢ ∃ (a' : ↥X), flip (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) a' x' ∧ f a' = y

Tactic:
obtain ⟨l, hl₁, hl₂⟩ := (H { R := A, K := X.residueField x', commSq := ⟨w⟩, .. }).exists_lift

Premises used: CategoryTheory.CommSq.HasLift.exists_lift